aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/extraargs.ml4
Commit message (Expand)AuthorAge
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\
| * Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
* | 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
* | Moving Ltac-specific parsing API to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-14
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Fixing printing of Register retroknowledge.Gravatar Hugo Herbelin2016-06-16
* 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
* Revert "Fixing printing of Register retroknowledge."Gravatar Hugo Herbelin2016-04-27
* Fixing printing of Register retroknowledge.Gravatar Hugo Herbelin2016-04-27
* Disentangle tactic notation resolution from Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Adding toplevel representation sharing for some generic arguments.Gravatar Pierre-Marie Pédrot2016-04-12
* Removing redundant *_TYPED AS clauses in EXTEND statements.Gravatar Pierre-Marie Pédrot2016-04-12
* Moving the code handling tactic notations to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
* 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-28 18:45:53 +0000