aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_tactics.mli
AgeCommit message (Expand)Author
2020-06-24Remove the catchable-exception related functions.Pierre-Marie Pédrot
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-13Deprecation of catchable_exception, to be replaced by noncritical in try-with.Hugo Herbelin
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-02Fix #5752: `Hint Mode` ignored for type classes that appear as assumptionsMaxime Dénès
2019-05-02Document typeclasses_eautoMaxime Dénès
2019-03-26Declare initial hint databases in preludeMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-27Post-rebase warnings (unused opens and 2 unused values)Gaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-24Removing various tactic compatibility layers in core tactics.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Removing most nf_enter in tactics.Pierre-Marie Pédrot
2017-02-14Class_tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Hints API using EConstr.Pierre-Marie Pédrot
2016-11-03Rework search_strategy option handlingMatthieu Sozeau
2016-11-03Internal API change to typeclasses eauto.Théo Zimmermann
2016-11-03Fix handling of only_classes at toplevelMatthieu Sozeau
2016-11-03Fix Typeclasses eauto := bfs.Matthieu Sozeau
2016-06-16Typeclasses:rename solve_instantiation* & use HookMatthieu Sozeau
2016-06-16Purely refactoring and code/API cleanup.Matthieu Sozeau
2016-06-16bteauto: a Proofview.tactic for multiple goalsMatthieu Sozeau
2016-06-16Typeclasses: refine the eauto tacticMatthieu Sozeau
2016-06-16Implement limited proof search and iterative deepening.Matthieu Sozeau
2016-06-16Typeclasses eauto based on new proof engine,Matthieu Sozeau
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-03-25Moving Eauto and Class_tactics to tactics/.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-04Splitting Class_tactics between code and CAMLP4/5 declarations.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:55 +0000