aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/extratactics.ml4
Commit message (Expand)AuthorAge
* Removing redundant *_TYPED AS clauses in EXTEND statements.Gravatar Pierre-Marie Pédrot2016-04-12
* Making Autorewrite independent from Ltac.Gravatar Pierre-Marie Pédrot2016-03-25
* Moving type_uconstr to Pretyping.Gravatar Pierre-Marie Pédrot2016-03-25
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21