aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Typeclasses.v
Commit message (Expand)AuthorAge
* Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
* Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
* Fix typeclasses eauto shelving.Gravatar Théo Zimmermann2016-11-30
* Revert more of a477dc for good measureGravatar Matthieu Sozeau2016-11-16
* Revert part of a477dc, disallow_shelvedGravatar Matthieu Sozeau2016-11-15
* typeclasses eauto Implem/doc of shelving strategyGravatar Matthieu Sozeau2016-11-03
* Fix handling of only_classes at toplevelGravatar Matthieu Sozeau2016-11-03
* Test new syntax for hints and typeclass optionsGravatar Matthieu Sozeau2016-11-03
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\
* | 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
* | Add an Iterative Deepening search strategy to typeclass resolution.Gravatar Matthieu Sozeau2015-07-27
|/
* test-suite: fix success/Typeclasses.vGravatar glondu2010-10-05
* Substitute terms for evars-as-goals as soon as they are solved inGravatar msozeau2009-11-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 20:50:02 +0000