aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tacsubst.ml
Commit message (Expand)AuthorAge
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* Fixing missing substitution / printing cases of TacSelect.Gravatar Pierre-Marie Pédrot2016-06-16
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar 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
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
* Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* Attempt to slightly improve abusive "Collision between boundGravatar Hugo Herbelin2016-04-27
* 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-12-02 13:13:07 +0000