aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.mli
Commit message (Expand)AuthorAge
* Add [guard] tactic.Gravatar Arnaud Spiwack2014-08-01
* The tactic interpreter now uses a new type of tactics, throughGravatar Pierre-Marie Pédrot2014-06-03
* Revert "Chasing the goal entering backward while interpreting tactics. This r...Gravatar Pierre-Marie Pédrot2014-05-24
* Chasing the goal entering backward while interpreting tactics. This requiredGravatar Pierre-Marie Pédrot2014-05-24
* Tactics declared through TACTIC EXTEND that are of the formGravatar Pierre-Marie Pédrot2014-05-20
* Adding phantom types to discriminate normalized goals, and adding a way toGravatar Pierre-Marie Pédrot2014-03-19
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Tacinterp: spurious enterl.Gravatar Arnaud Spiwack2014-02-27
* Dead code: eval_ltac_constr.Gravatar Arnaud Spiwack2014-02-27
* Do not use ugly Dyn features in the Quote plugin. Use instead theGravatar Pierre-Marie Pédrot2013-11-26
* Tacinterp: fewer use of old-style goals.Gravatar Arnaud Spiwack2013-11-25
* Centralizing the Ltac-defining functions in Tacenv.Gravatar ppedrot2013-11-10
* Made multiple-goal tactic work after all: .Gravatar aspiwack2013-11-02
* Getting rid of Goal.here, and all the related exceptions and combinators.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Cleaning up the type of Tacinterp.extract_ltac_constr_values.Gravatar ppedrot2013-06-24
* Now, idtac closures use maps instead of association list.Gravatar ppedrot2013-06-22
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Removing the various glob/subst/interp registering functions forGravatar ppedrot2013-06-18
* Now glob_sign and interp_sign only depend on structures definedGravatar ppedrot2013-06-18
* Exporting field f_debug (needed for Ssreflect).Gravatar ppedrot2013-06-14
* Using an "extra" Store.t field in interp_sign instead of dedicatedGravatar ppedrot2013-06-14
* Moving coercion functions out of Tacinterp.Gravatar ppedrot2013-06-12
* Hiding tactic value representations.Gravatar ppedrot2013-06-10
* Replacing lists by maps in matching interpretation.Gravatar ppedrot2013-06-05
* Make ist (interp_sign) available to TACTIC EXTEND codeGravatar gareuselesinge2013-05-29
* Modulification of identifierGravatar ppedrot2012-12-14
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* Updating headers.Gravatar herbelin2012-08-08
* Dump references in reduction tacticsGravatar pboutill2012-08-05
* 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
* 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
* Corrects a (very) longstanding bug of tactics. As is were, tactic expectingGravatar aspiwack2012-04-18
* Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicGravatar herbelin2012-03-20
* Noise for nothingGravatar pboutill2012-03-02
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
* Moving implicit tactic support from Tacinterp to Pfedit and final evarGravatar herbelin2011-09-26
* Rename subst_raw_with_bindings to subst_glob_with_bindings and exportGravatar msozeau2011-02-10
* One more fix for setoid_rewrite: completely reinterpret the given lemmasGravatar msozeau2011-02-09
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar 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
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06