aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.mli
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Removing various tactic compatibility layers in core tactics.Gravatar Pierre-Marie Pédrot2017-04-24
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Class_tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Rework search_strategy option handlingGravatar Matthieu Sozeau2016-11-03
| * Internal API change to typeclasses eauto.Gravatar Théo Zimmermann2016-11-03
| * Fix handling of only_classes at toplevelGravatar Matthieu Sozeau2016-11-03
| * Fix Typeclasses eauto := bfs.Gravatar Matthieu Sozeau2016-11-03
|/
* 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