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

6 files changed, 15 insertions, 37 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 58ae7191f8..7c4bd4d201 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -392,13 +392,12 @@ than {\tt eauto} and {\tt auto}. The main differences are the following:
   backtracking on subgoals that are entirely independent.
 \item When called with no arguments, {\tt typeclasses eauto} uses the
   {\tt typeclass\_instances} database by default (instead of {\tt core})
-  and will try to solve \emph{only} typeclass goals. If some subgoal of
-  a hint/instance is non-dependent and not of class type, that hint
-  application will fail. Dependent subgoals are automatically shelved
-  and \emph{must be} resolved entirely when the other typeclass subgoals
-  are resolved or the proof search will fail \emph{globally},
-  \emph{without} the possibility to find another complete solution with
-  no shelved subgoals.
+  and will try to solve \emph{only} typeclass goals, shelving the other
+  goals. If some subgoal of a hint/instance is non-dependent and not of
+  class type, the hint application will fail when faced with that
+  subgoal. Dependent subgoals are automatically shelved, and shelved
+  goals can remain after resolution ends (following the behavior of
+  \Coq{} 8.5).
 
   \emph{Note: } As of Coq 8.6, {\tt all:once (typeclasses eauto)}
   faithfully mimicks what happens during typeclass resolution when it is
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 262b308932..99a1a98993 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1176,7 +1176,7 @@ module Search = struct
              (fun e' ->
 	      if CErrors.noncritical (fst e') then
                 (pr_error e'; aux (merge_exceptions e e') tl)
-              else (Printf.printf "raising again\n%!"; iraise e'))
+              else iraise e')
     and aux e = function
       | x :: xs -> onetac e x xs
       | [] ->
@@ -1274,27 +1274,6 @@ module Search = struct
                                    | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
-  let disallow_shelved initshelf tac =
-    let open Proofview in
-    let casefn = function
-    | Fail (e,info) -> tclZERO ~info e
-    | Next ((shelved, result), k) ->
-       if not (List.is_empty shelved) then
-         begin
-           Proofview.tclEVARMAP >>= fun sigma ->
-	   let gls = prlist_with_sep spc (pr_ev sigma) shelved in
-	   (if !typeclasses_debug > 0 then
-	      let initgls = prlist_with_sep spc (pr_ev sigma) initshelf in
-	      Feedback.msg_debug (str"Non-empty shelf at end of resolution:" ++ gls
-                                  ++ str" initially: " ++ initgls ++ str"."));
-	   Tacticals.New.tclZEROMSG (str"Proof search failed: " ++
-				      str"shelved goals remain: " ++ gls)
-         end
-       else
-         tclOR (tclUNIT result) (fun e -> k e >>= fun (gls, result) -> tclUNIT result)
-    in
-    tclCASE (with_shelf tac) >>= casefn
-
   let eauto_tac ?(st=full_transparent_state) ?(unique=false)
                 ~only_classes ?strategy ~depth ~dep hints =
     let open Proofview in
@@ -1342,7 +1321,6 @@ module Search = struct
                                str " in regular mode" ++
                                  match depth with None -> str ", unbounded"
                                                 | Some i -> str ", with depth limit " ++ int i));
-    let tac = if only_classes then disallow_shelved initshelf tac else tac in
     tac
 
   let run_on_evars p evm tac =
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.