aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/g_ltac.ml4
Commit message (Expand)AuthorAge
* Adding the Print Ltac Signature command.Gravatar Pierre-Marie Pédrot2016-06-05
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"Gravatar Hugo Herbelin2016-04-27
* Revert "Typo in comment."Gravatar Hugo Herbelin2016-04-27
* Typo in comment.Gravatar Hugo Herbelin2016-04-27
* Fixing parsing of constr argument of ltac functions at level 8 in theGravatar Hugo Herbelin2016-04-27
* Higher-level API for tactic notations.Gravatar Pierre-Marie Pédrot2016-04-24
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
* Removing extra spaces in printing arguments of VERNAC EXTEND.Gravatar Hugo Herbelin2016-04-09
* Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...Gravatar Hugo Herbelin2016-04-09
* 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-29 17:13:12 +0000