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

1 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 3178c6fc1..0af367781 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.