aboutsummaryrefslogtreecommitdiff
path: root/printing/pptactic.ml
AgeCommit message (Expand)Author
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-04Removing the UConstr entry of the tactic_arg AST.Pierre-Marie Pédrot
2016-02-29Moving the "move" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "exists" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "symmetry" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "generalize dependent" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clearbody" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clear" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "cofix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "fix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-24Removing the MetaIdArg entry of tactic expressions.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
2016-01-17Getting rid of the awkward unpack mechanism from Genarg.Pierre-Marie Pédrot
2016-01-17Temporary commit getting rid of Obj.magic unsafety for Genarg.Pierre-Marie Pédrot
2016-01-16Tactic notation printing accesses all the token data.Pierre-Marie Pédrot
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-14Removing ident and var generic arguments.Pierre-Marie Pédrot
2016-01-02Remove some unused functions.Guillaume Melquiond
2016-01-02Remove useless rec flags.Guillaume Melquiond
2016-01-02Separation of concern in TacAlias API.Pierre-Marie Pédrot
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
2015-12-28Removing the special status of open_constr generic argument.Pierre-Marie Pédrot
2015-12-27Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Pierre-Marie Pédrot
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-21Removing ad-hoc interpretation rules for tactic notations and their genarg.Pierre-Marie Pédrot
2015-12-21Changing the toplevel type of the int_or_var generic type to int.Pierre-Marie Pédrot
2015-12-21Removing the now useless genarg generic argument.Pierre-Marie Pédrot
2015-12-18Tying the loop in tactic printing API.Pierre-Marie Pédrot
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
2015-12-04Getting rid of the dynamic node of the tactic AST.Pierre-Marie Pédrot
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-10-19Type delayed_open_constr is now monotonic.Pierre-Marie Pédrot
2015-06-25Remove other types not carried by interpretations in `Tacexpr`.Arnaud Spiwack
2015-06-25Remove useless `and_short_name` in interpreted level in `Tacexpr`.Arnaud Spiwack
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-01-23Splitting ML tactics in one function per grammar entry.Pierre-Marie Pédrot
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-18Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-23A global [gfail] tactic which works like [fail] except that it fails even if ...Arnaud Spiwack
2014-12-23Fix compilation error in some configurations.Arnaud Spiwack
2014-12-19Add a backtracking version of Ltac's [match].Arnaud Spiwack
2014-12-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-11-19Print [uconstr] in genargs.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 06:04:30 +0000