aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/g_class.ml4
Commit message (Expand)AuthorAge
* Rework search_strategy option handlingGravatar Matthieu Sozeau2016-11-03
* Fix Typeclasses eauto := bfs.Gravatar Matthieu Sozeau2016-11-03
* Fix bug #5093: typeclasses eauto depth arg does not accept a var.Gravatar Pierre-Marie Pédrot2016-09-26
* Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
* bteauto: a Proofview.tactic for multiple goalsGravatar 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
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21