aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* Fix auto so that Extern tactics associated to no patterns can apply toGravatar msozeau2009-03-31
* Compromise wrt introduction-names compatibility issue after additionGravatar herbelin2009-03-22
* Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)Gravatar herbelin2009-03-17
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* 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
* 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
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* - 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
* - 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
* Fixed in bug in previous 11662 (incorrect with_evars flag in descend_conjunct...Gravatar herbelin2008-12-12
* About "apply in":Gravatar herbelin2008-12-09
* closed bug 1898: fold x in x; added a reordering primitive tacticGravatar barras2008-11-26
* - Fixed minor bug #1994 in the tactic chapter of the manual [doc]Gravatar herbelin2008-11-22
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* 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
* Fix bug #1977 by allowing the [apply] variants to take an [open_constr]Gravatar msozeau2008-10-23
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Various little improvements:Gravatar msozeau2008-09-25
* 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 bug #1935, reworking the reflexivity, symmetry... tactics to useGravatar msozeau2008-09-03
* Fixes in dependent induction tactic to keep names, allow givingGravatar msozeau2008-08-21
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
* New tactics [conv] to test convertibility (actually, unification) of twoGravatar msozeau2008-07-22
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Backtrack sur l'"optimisation" de admit (révision 11084). Comme leGravatar herbelin2008-06-10
* - Correction bug 1841 (identificateurs incorrects avec Subclass)Gravatar herbelin2008-06-10
* - Patch sur "intros until 0"Gravatar herbelin2008-06-08
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Improve the dependent induction tactic to automatically find theGravatar msozeau2008-05-30
* Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757Gravatar herbelin2008-05-07
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-25 18:44:24 +0000