| Age | Commit message (Expand) | Author |
|---|
| 2008-12-12 | Fixed in bug in previous 11662 (incorrect with_evars flag in descend_conjunct... | herbelin |
| 2008-12-09 | About "apply in": | herbelin |
| 2008-12-04 | Do not catch _all_ exceptions in setoid unification. | msozeau |
| 2008-11-26 | closed bug 1898: fold x in x; added a reordering primitive tactic | barras |
| 2008-11-23 | Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b | herbelin |
| 2008-11-22 | - Fixed minor bug #1994 in the tactic chapter of the manual [doc] | herbelin |
| 2008-11-10 | Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] not | msozeau |
| 2008-11-09 | More factorization of inductive/record and typeclasses: move class | msozeau |
| 2008-11-09 | - Fixed bug 1968 (inversion failing due to a Not_found bug introduced in | herbelin |
| 2008-11-07 | Add the ability to give a specific tactic to solve each obligation in | msozeau |
| 2008-11-05 | Port [rewrite] tactics to open terms. Currently no check that evars | msozeau |
| 2008-11-04 | Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974) | herbelin |
| 2008-10-29 | Adaptation du vieil appel à "apply" sur lemme de symétrie au cas où | herbelin |
| 2008-10-27 | - Fixed many "Theorem with" bugs. | herbelin |
| 2008-10-26 | Fixes and refinements regarding occurrence selection: | herbelin |
| 2008-10-26 | Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui | herbelin |
| 2008-10-25 | More debugging of handling of open constrs with typeclasses: | msozeau |
| 2008-10-23 | Forgot one file which had other local modifications... | msozeau |
| 2008-10-23 | Fix bug #1977 by allowing the [apply] variants to take an [open_constr] | msozeau |
| 2008-10-23 | Generalized implementation of generalization. | msozeau |
| 2008-10-22 | Affichage des notations récursives: | herbelin |
| 2008-10-19 | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin |
| 2008-10-18 | Fixed bug #1966, wrong handling of evars. | msozeau |
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-10-11 | Backporting 11445 from 8.2 to trunk (negative conditions in | herbelin |
| 2008-09-25 | Various little improvements: | msozeau |
| 2008-09-25 | Partial fix for bug #1948: recompute order of dependencies between | msozeau |
| 2008-09-14 | Add user syntax for creating hint databases [Create HintDb foo | msozeau |
| 2008-09-14 | Fix bug #1936: uncaught exception due to undefinable exceptions. | msozeau |
| 2008-09-14 | Fix bug #1939: defined evars were not substituted in some typeclasses | msozeau |
| 2008-09-13 | Remove redefinition of id in Program.Basics, just add maximal implicits. | msozeau |
| 2008-09-12 | Add a type argument to letin_tac instead of using casts and recomputing | msozeau |
| 2008-09-11 | Fixes in dependent induction tactic, putting things in better order for | msozeau |
| 2008-09-09 | Fix a bug reintroduced in [setoid_reflexivity] etc... | msozeau |
| 2008-09-07 | Add the ability to declare [Hint Extern]'s with no pattern. | msozeau |
| 2008-09-07 | Fixes in typeclasses resolution. Avoid reducing instances types before | msozeau |
| 2008-09-07 | Small fixes in "varify", a small tactic doing the first part of | msozeau |
| 2008-09-07 | Better handling of the opacity of proof obligations, add the possibility of | msozeau |
| 2008-09-04 | Improve typeclasses eauto using the dnet for local assumptions too, and select | msozeau |
| 2008-09-04 | Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving an | msozeau |
| 2008-09-03 | Fix bug #1935, reworking the reflexivity, symmetry... tactics to use | msozeau |
| 2008-09-02 | Initial implementation of a new command to define (dependent) functions by | msozeau |
| 2008-08-27 | Major speed and space improvements in setoid rewrite: | msozeau |
| 2008-08-27 | Little cleanup in auto. | msozeau |
| 2008-08-22 | - New auto hints for transparency/opacity control, not bound to | msozeau |
| 2008-08-21 | Fixes in dependent induction tactic to keep names, allow giving | msozeau |
| 2008-08-05 | Correction de bugs: | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-28 | Fixes in generalize_eqs/dependent induction to allow the user to specify | msozeau |
| 2008-07-28 | Fix wrong environment bug in test for setoid_rewrite or rewrite. | msozeau |
