aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/Typeclasses.v
AgeCommit message (Expand)Author
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-06-29[test-suite] async-proofs off in tests with Fail TimeoutEnrico Tassi
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2016-11-30Fix typeclasses eauto shelving.Théo Zimmermann
2016-11-16Revert more of a477dc for good measureMatthieu Sozeau
2016-11-15Revert part of a477dc, disallow_shelvedMatthieu Sozeau
2016-11-03typeclasses eauto Implem/doc of shelving strategyMatthieu Sozeau
2016-11-03Fix handling of only_classes at toplevelMatthieu Sozeau
2016-11-03Test new syntax for hints and typeclass optionsMatthieu Sozeau
2016-10-12Merge branch 'v8.5' into v8.6Pierre-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
2015-07-27Add an Iterative Deepening search strategy to typeclass resolution.Matthieu Sozeau
2010-10-05test-suite: fix success/Typeclasses.vglondu
2009-11-27Substitute terms for evars-as-goals as soon as they are solved inmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:03:19 +0000