aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tacentries.mli
Commit message (Expand)AuthorAge
* Adding the Print Ltac Signature command.Gravatar Pierre-Marie Pédrot2016-06-05
* Pass user symbol to tactic notation printers.Gravatar Pierre-Marie Pédrot2016-05-08
* Documenting API.Gravatar Pierre-Marie Pédrot2016-04-25
* 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
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
* 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