aboutsummaryrefslogtreecommitdiff
path: root/ltac/extratactics.ml4
AgeCommit message (Expand)Author
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Removing useless generic arguments.Pierre-Marie Pédrot
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-04-12Removing redundant *_TYPED AS clauses in EXTEND statements.Pierre-Marie Pédrot
2016-03-25Making Autorewrite independent from Ltac.Pierre-Marie Pédrot
2016-03-25Moving type_uconstr to Pretyping.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot