aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.mli
Commit message (Expand)AuthorAge
* Writing [cut] tactic using the new monad.Gravatar Pierre-Marie Pédrot2013-12-02
* Remove the Hiddentac module.Gravatar Arnaud Spiwack2013-11-25
* Porting Tactics.assumption to the new engine.Gravatar ppedrot2013-11-08
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as anGravatar herbelin2013-06-02
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* 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