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

4 files changed, 8 insertions, 7 deletions

diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index ff515038ec..9ed0926a66 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -89,5 +89,6 @@ Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred)
   Show Existentials.
   Set Typeclasses Debug Verbosity 2.
   Set Printing All.
-  Fail apply reflexivity.
+  (* As in 8.5, allow a shelved subgoal to remain *)
+  apply reflexivity.
   
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v
index 83d4ed69d4..ffd33d3813 100644
--- a/test-suite/bugs/closed/4095.v
+++ b/test-suite/bugs/closed/4095.v
@@ -1,10 +1,10 @@
 (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines, then from 92 lines to 79 lines *)
 (* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
-Require Import TestSuite.admit.
 Require Import Coq.Setoids.Setoid.
 Generalizable All Variables.
 Axiom admit : forall {T}, T.
+Ltac admit := apply admit.
 Class Equiv (A : Type) := equiv : relation A.
 Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv.
 Class ILogicOps Frm := { lentails: relation Frm;
@@ -71,7 +71,7 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     refine (P _ _)
   end.
   Undo.
-  lazymatch goal with
+  Fail lazymatch goal with
   | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
     let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in
     set(p:=P)
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.