aboutsummaryrefslogtreecommitdiff
path: root/ltac/g_class.ml4
AgeCommit message (Expand)Author
2016-11-03Rework search_strategy option handlingMatthieu Sozeau
2016-11-03Fix Typeclasses eauto := bfs.Matthieu Sozeau
2016-09-26Fix bug #5093: typeclasses eauto depth arg does not accept a var.Pierre-Marie Pédrot
2016-06-16Purely refactoring and code/API cleanup.Matthieu Sozeau
2016-06-16bteauto: a Proofview.tactic for multiple goalsMatthieu Sozeau
2016-06-16Implement limited proof search and iterative deepening.Matthieu Sozeau
2016-06-16Typeclasses eauto based on new proof engine,Matthieu Sozeau
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot