aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tacentries.ml
Commit message (Expand)AuthorAge
* A fix to #3709: ensuring extra parentheses when a tactic entry has aGravatar Hugo Herbelin2016-04-27
* Merging the ML tactic notation and plain Tactic Notation mechanisms.Gravatar Pierre-Marie Pédrot2016-04-25
* Factorizing code in tactic notations.Gravatar Pierre-Marie Pédrot2016-04-25
* Documenting API.Gravatar Pierre-Marie Pédrot2016-04-25
* Remove dead registering code in Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Disentangle tactic notation resolution from Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Higher-level API for tactic notations.Gravatar Pierre-Marie Pédrot2016-04-24
* Factorizing the declaration of ML notation printing in Tacentries.Gravatar Pierre-Marie Pédrot2016-04-24
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
* Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
* Moving the code handling tactic notations to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
* Moving the Tactic Notation entry parser from Pcoq 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-07-02 04:50:42 +0000