aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.mli
Commit message (Expand)AuthorAge
* Typeclasses:rename solve_instantiation* & use HookGravatar Matthieu Sozeau2016-06-16
* Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
* bteauto: a Proofview.tactic for multiple goalsGravatar Matthieu Sozeau2016-06-16
* Typeclasses: refine the eauto tacticGravatar Matthieu Sozeau2016-06-16
* Implement limited proof search and iterative deepening.Gravatar Matthieu Sozeau2016-06-16
* Typeclasses eauto based on new proof engine,Gravatar Matthieu Sozeau2016-06-16
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Moving Eauto and Class_tactics to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Splitting Class_tactics between code and CAMLP4/5 declarations.Gravatar ppedrot2013-10-04