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