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