aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacinterp.mli
AgeCommit message (Expand)Author
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-03-06Moving Ltac traces to Tacexpr and Tacinterp.Pierre-Marie Pédrot
2016-02-22The tactic generic argument now returns a value rather than a glob_expr.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-28Implementing non-focussed generic arguments.Pierre-Marie Pédrot
2015-12-27Factorizing code for untyped constr evaluation.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-04Getting rid of the dynamic node of the tactic AST.Pierre-Marie Pédrot
2015-12-03Removing the globTacticIn primitive.Pierre-Marie Pédrot
2015-12-03Removing the last use of tacticIn in setoid_ring.Pierre-Marie Pédrot
2015-12-03Removing the use of tacticIn in Tauto.Pierre-Marie Pédrot
2015-12-02Removing dead code in Obligations.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-09-06Proper interpretation function for tauto.Pierre-Marie Pédrot
2014-09-06Adding a way to inject tactic closures in interpretation values.Pierre-Marie Pédrot
2014-08-01Add [guard] tactic.Arnaud Spiwack
2014-06-03The tactic interpreter now uses a new type of tactics, throughPierre-Marie Pédrot
2014-05-24Revert "Chasing the goal entering backward while interpreting tactics. This r...Pierre-Marie Pédrot
2014-05-24Chasing the goal entering backward while interpreting tactics. This requiredPierre-Marie Pédrot
2014-05-20Tactics declared through TACTIC EXTEND that are of the formPierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:45:07 +0000