diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-11-15 13:53:57 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-11-15 14:54:05 +0100 |
| commit | 4b8f19c58a2b6cc841db2c011d23aa8106211fd6 (patch) | |
| tree | ade3adfabf9e288a164769e0457fda6e49ac1b24 /test-suite/success/Typeclasses.v | |
| parent | dfefd12ee432e5b0d145934e74bb939ddecfa522 (diff) | |
Revert part of a477dc, disallow_shelved
In only_classes mode we do not try to implement a stricter semantics for
shelved goals in 8.6. Leaving this for 8.7.
Update the documentation as well.
Remove a spurious printf call as well.
Fix test-suite now that shelved goals are allowed
Diffstat (limited to 'test-suite/success/Typeclasses.v')
| -rw-r--r-- | test-suite/success/Typeclasses.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 6885717ec..5557ba837 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -6,7 +6,7 @@ Module onlyclasses. Goal Foo * Foo. split. shelve. Set Typeclasses Debug. - Fail typeclasses eauto. + Fail (unshelve typeclasses eauto); fail. typeclasses eauto with typeclass_instances. Unshelve. typeclasses eauto with typeclass_instances. Qed. |