aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/g_auto.ml4
Commit message (Expand)AuthorAge
* Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
* Typeclasses eauto based on new proof engine,Gravatar Matthieu Sozeau2016-06-16
* Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Gravatar Hugo Herbelin2016-04-27
* Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-04-27
* Removing redundant *_TYPED AS clauses in EXTEND statements.Gravatar Pierre-Marie Pédrot2016-04-12
* 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