Merge remote-tracking branch 'github/pr/358' into v8.6

Was PR#358: Revert part of a477dc, disallow_shelved

2 files changed, 4 insertions, 4 deletions

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 6885717ec5..5557ba8379 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.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 3178c6fc15..0af367781a 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -24,9 +24,9 @@ Module Backtracking.
     Fail all:((once (typeclasses eauto with typeclass_instances))
               + apply eq_refl).
     (* Does backtrack if other goals fail *)
-    all:[> typeclasses eauto + reflexivity .. ].
+    all:[> (unshelve typeclasses eauto; fail) + reflexivity .. ].
     Undo 1.
-    all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *)
+    all:((unshelve typeclasses eauto; fail) + reflexivity). (* Note "+" is a focussing combinator *)
     Show Proof.  
   Qed.
 
@@ -66,7 +66,7 @@ Module Backtracking.
       unshelve evar (t : A). all:cycle 1.
       refine (@ex_intro _ _ t _).
       all:cycle 1.
-      all:(typeclasses eauto + reflexivity).
+      all:((unshelve typeclasses eauto; fail) + reflexivity).
     Qed.      
   End Leivant.
 End Backtracking.