aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.mli
Commit message (Expand)AuthorAge
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
* Exported tactic intro_thenGravatar herbelin2011-08-10
* Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...Gravatar herbelin2011-07-16
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Removing redundant internal variants of apply tactic and simplification of ML...Gravatar herbelin2010-04-14
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* Added "etransitivity".Gravatar herbelin2009-08-03
* Reimplementation of leibniz rewrite to control the instantiation of theGravatar msozeau2009-06-16
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* 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
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
* About "apply in":Gravatar herbelin2008-12-09
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* Fixes and refinements regarding occurrence selection:Gravatar 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
* Fix bug #1935, reworking the reflexivity, symmetry... tactics to useGravatar msozeau2008-09-03
* É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
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
* Added a function to rebuild an elim scheme from elim_scheme_info. WillGravatar courtieu2008-03-18
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30