aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacinterp.mli
AgeCommit message (Expand)Author
2014-03-19Adding phantom types to discriminate normalized goals, and adding a way toPierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-27Tacinterp: spurious enterl.Arnaud Spiwack
2014-02-27Dead code: eval_ltac_constr.Arnaud Spiwack
2013-11-26Do not use ugly Dyn features in the Quote plugin. Use instead thePierre-Marie Pédrot
2013-11-25Tacinterp: fewer use of old-style goals.Arnaud Spiwack
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
2013-11-02Made multiple-goal tactic work after all: .aspiwack
2013-11-02Getting rid of Goal.here, and all the related exceptions and combinators.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-06-24Cleaning up the type of Tacinterp.extract_ltac_constr_values.ppedrot
2013-06-22Now, idtac closures use maps instead of association list.ppedrot
2013-06-22Generalizing the use of maps instead of lists in the interpretationppedrot
2013-06-21Splitted up Genarg in four different levels:ppedrot
2013-06-18Removing the various glob/subst/interp registering functions forppedrot
2013-06-18Now glob_sign and interp_sign only depend on structures definedppedrot
2013-06-14Exporting field f_debug (needed for Ssreflect).ppedrot
2013-06-14Using an "extra" Store.t field in interp_sign instead of dedicatedppedrot
2013-06-12Moving coercion functions out of Tacinterp.ppedrot
2013-06-10Hiding tactic value representations.ppedrot
2013-06-05Replacing lists by maps in matching interpretation.ppedrot
2013-05-29Make ist (interp_sign) available to TACTIC EXTEND codegareuselesinge
2012-12-14Modulification of identifierppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-08-08Updating headers.herbelin
2012-08-05Dump references in reduction tacticspboutill
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-04-18Corrects a (very) longstanding bug of tactics. As is were, tactic expectingaspiwack
2012-03-20Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicherbelin
2012-03-02Noise for nothingpboutill
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-02-10Rename subst_raw_with_bindings to subst_glob_with_bindings and exportmsozeau
2011-02-09One more fix for setoid_rewrite: completely reinterpret the given lemmasmsozeau
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-14Fixed commit 13125 (stricter check of induction args): an interpretationherbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-12-21Generic support for open terms in tacticsherbelin
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 10:47:06 +0000