aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Backtrack sur la mémoïsation de nf_evar.Gravatar aspiwack2009-03-04
* =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...Gravatar aspiwack2009-02-27
* Add support for dependent "destruct" over terms in dependent types.Gravatar herbelin2009-02-23
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Fix [apply_in] which short-circuited resolution of evars in a customGravatar msozeau2009-02-16
* pushed evar reduction in kernelGravatar barras2009-02-06
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
* Solves some warning and hides some not-bad ones in doc. It remains aGravatar herbelin2009-01-29
* Petit nettoyage faisant suite au commit #11847 .Gravatar aspiwack2009-01-23
* Fix bug #2004 due to bad handling of evars in the unification for Gravatar msozeau2009-01-21
* Various little fixes:Gravatar msozeau2009-01-18
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
* Fix a bunch of bugs related to setoid_rewrite, unification and evars:Gravatar msozeau2009-01-12
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* Fixed two problems:Gravatar herbelin2009-01-03
* - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",Gravatar herbelin2009-01-02
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* - Fixed bug #2021 (uncaught exception with injection/discriminate whenGravatar herbelin2009-01-01
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* - Fixed bugs and compatibilities issues in Gravatar herbelin2008-12-30
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* - Extracted from the tactic "now" an experimental tactic "easy" for smallGravatar herbelin2008-12-26
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 09:55:35 +0000