aboutsummaryrefslogtreecommitdiff
path: root/ltac/tacintern.ml
AgeCommit message (Expand)Author
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-09-15Generalizing the notion of constr substitution to generic arguments.Pierre-Marie Pédrot
2016-09-08Making Hints generic in the use of external tactics.Pierre-Marie Pédrot
2016-09-08Making Vernacexpr independent from Tacexpr.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-04Revert "Revert "Improve the interpretation scope of arguments of an ltac matc...Maxime Dénès
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-16A stronger invariant on the syntax of TacAssert, what allows for aHugo Herbelin
2016-06-14Goal selectors are now tacticals and can be used as such.Cyprien Mangin
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-03Removing "rename" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "exact" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "double induction" from the tactic AST.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Removing useless generic arguments.Pierre-Marie Pédrot
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Honor parsing and printing levels for tactic entry in TACTIC EXTEND andHugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
2016-04-27Attempt to slightly improve abusive "Collision between boundHugo Herbelin
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 22:26:07 +0000