aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/g_auto.ml4
Commit message (Expand)AuthorAge
* Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Gravatar Pierre-Marie Pédrot2015-12-28
* Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24