aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.mli
Commit message (Expand)AuthorAge
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 20:15:05 +0000