aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacentries.ml
Commit message (Expand)AuthorAge
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
* Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-03-17
|\
* | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
| * TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-02-24
|/
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17