- Jan 04, 2017
-
-
Robbert Krebbers authored
-
- Jan 03, 2017
-
-
Ralf Jung authored
This patch was created using find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 ' and some minor manual editing
-
- Dec 09, 2016
-
-
Ralf Jung authored
-
- Nov 29, 2016
-
-
Robbert Krebbers authored
-
- Nov 23, 2016
-
-
Robbert Krebbers authored
-
- Nov 21, 2016
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Nov 20, 2016
-
-
Robbert Krebbers authored
-
- Oct 03, 2016
-
-
Robbert Krebbers authored
-
- Sep 20, 2016
-
-
Robbert Krebbers authored
This also solves a name clash with the extension order of CMRAs.
-
- Aug 08, 2016
-
-
Ralf Jung authored
With Coq 8.6, you can no longer have intro patterns that give more names than the constructor has. Also, patterns with too few names are now interpreted as filling up with "?", rather than putting the unnamed parts into the goal again. Furthermore, it seems the behavior of "simplify_eq/=" changed, I guess hypotheses are considered in different order now. I managed to work around this, but it all seem kind of fragile. The next compilation failure is an "Anyomaly: ... Please report", so that's what I will do.
-
- Aug 02, 2016
-
-
Robbert Krebbers authored
-
- Jul 27, 2016
-
-
Robbert Krebbers authored
-
- Jul 22, 2016
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
There was not really a need for the lattice type classes, so I removed these.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
These just make things more complicated, it would be more useful to declare (efficient) decision procedures for each instance, so that we can properly predict which instance we will get.
-
- Jul 12, 2016
-
-
Robbert Krebbers authored
-
- Jul 11, 2016
-
-
Robbert Krebbers authored
This class whose name is horrible and purpose is arbitrary seems to be a leftover of some experiment with ch2o, a long time a ago.
-
- Jul 05, 2016
-
-
Robbert Krebbers authored
-
- May 31, 2016
-
-
Robbert Krebbers authored
-
- Mar 23, 2016
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- Mar 10, 2016
-
-
Robbert Krebbers authored
Thanks to Amin Timany for the suggestion.
-
- Mar 05, 2016
- Mar 04, 2016
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Mar 03, 2016
-
-
Robbert Krebbers authored
-
- Feb 24, 2016
-
-
Robbert Krebbers authored
It now traverses terms at most once, whereas the setoid_rewrite approach was travering terms many times. Also, the tactic can now be extended by defining type class instances.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Also, use "set_solver by tac" to specify a tactic.
-
- Feb 22, 2016
-
-
Robbert Krebbers authored
In most cases there is a lot of duplicate proof search performed by both naive_solver and eauto. Especially since naive_solver calls its tactic (in the case of set_solver this used to be eauto) quite eagerly this made it very slow. Note that set_solver is this too slow and should be improved.
-
Robbert Krebbers authored
In most cases there is a lot of duplicate proof search performed by both naive_solver and eauto. Especially since naive_solver calls its tactic (in the case of set_solver this used to be eauto) quite eagerly this made it very slow. Note that set_solver is this too slow and should be improved.
-
- Feb 17, 2016
-
-
Robbert Krebbers authored
It is doing much more than just dealing with ∈, it solves all kinds of goals involving set operations (including ≡ and ⊆).
-
Robbert Krebbers authored
simplify_equality => simplify_eq simplify_equality' => simplify_eq/= simplify_map_equality => simplify_map_eq simplify_map_equality' => simplify_map_eq/= simplify_option_equality => simplify_option_eq simplify_list_equality => simplify_list_eq f_equal' => f_equal/= The /= suffixes (meaning: do simpl) are inspired by ssreflect.
-
Robbert Krebbers authored
-
- Feb 16, 2016
-
-
Ralf Jung authored
-
- Feb 15, 2016
-
-
Robbert Krebbers authored
-