Revert more of a477dc for good measure

We stop failing automatically on non-declared-class nested or toplevel
subgoals as in 8.5, instead of the previous a477dc behavior of shelving
those goals and failing if shelved goals remained at the end of
resolution. It means typeclass resolution during refinement is closer to
all:typeclasses eauto. Hints in typeclass_instances for non-declared
classes can be used during resolution of _nested_ subgoals when it is
fired from type-inference, toplevel goals considered in this case are
still only classes (as in 8.5 and before). The code that triggers the
restriction to only declared class subgoals is commented.

Revert changes to test-suite, adding test for #5203, #5198 is fixed too.

Add corresponding tests in the test-suite (that will break if we,
e.g. disallow non-class subgoals) and update the refman accordingly.

6 files changed, 99 insertions, 20 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 7c4bd4d20..bd8ee450e 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -391,19 +391,19 @@ than {\tt eauto} and {\tt auto}. The main differences are the following:
   It analyses the dependencies between subgoals to avoid
   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, 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
+  {\tt typeclass\_instances} database by default (instead of {\tt
+    core}).
+  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
-  called during refinement/type-inference. It might move to {\tt
-    all:typeclasses eauto} in future versions when the refinement engine
-  will be able to backtrack.
+  called during refinement/type-inference, except that \emph{only}
+  declared class subgoals are considered at the start of resolution
+  during type inference, while ``all'' can select non-class subgoals as
+  well. It might move to {\tt all:typeclasses eauto} in future versions
+  when the refinement engine will be able to backtrack.
 \item When called with specific databases (e.g. {\tt with}), {\tt
     typeclasses eauto} allows shelved goals to remain at any point
   during search and treat typeclasses goals like any other.
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 99a1a9899..4138562c6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1167,7 +1167,8 @@ module Search = struct
       if path_matches derivs [] then aux e tl
       else
         let filter =
-          if info.search_only_classes then fail_if_nonclass info
+          if false (* in 8.6, still allow non-class subgoals
+                    info.search_only_classes *) then fail_if_nonclass info
           else Proofview.tclUNIT ()
         in
         ortac
@@ -1238,8 +1239,8 @@ module Search = struct
         unit Proofview.tactic =
     let open Proofview in
     let open Proofview.Notations in
-    if only_classes && not (is_class_type sigma (Goal.concl gl)) then
-      Proofview.shelve
+    if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
+      Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
     else
       let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
       let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v
new file mode 100644
index 000000000..7254afb42
--- /dev/null
+++ b/test-suite/bugs/closed/5198.v
@@ -0,0 +1,39 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 286 lines to 
+27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, 
+then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from 
+253 lines to 65 lines, then from 79 lines to 65 lines *)
+(* coqc version 8.6.0 (November 2016) compiled on Nov 12 2016 14:43:52 with 
+OCaml 4.02.3
+   coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-v8.6,v8.6 
+(7e992fa784ee6fa48af8a2e461385c094985587d) *)
+Axiom admit : forall {T}, T.
+Set Printing Implicit.
+Inductive nat := O | S (_ : nat).
+Axiom f : forall (_ _ : nat), nat.
+Class ZLikeOps (e : nat)
+  := { LargeT : Type ; SmallT : Type ; CarryAdd : forall (_ _ : LargeT), LargeT 
+}.
+Class BarrettParameters :=
+  { b : nat ; k : nat ; ops : ZLikeOps (f b k) }.
+Axiom barrett_reduce_function_bundled : forall {params : BarrettParameters}
+                                               (_ : @LargeT _ (@ops params)),
+    @SmallT _ (@ops params).
+
+Global Instance ZZLikeOps e : ZLikeOps (f (S O) e)
+  := { LargeT := nat ; SmallT := nat ; CarryAdd x y := y }.
+Definition SRep := nat.
+Local Instance x86_25519_Barrett : BarrettParameters
+  := { b := S O ; k := O ; ops := ZZLikeOps O }.
+Definition SRepAdd : forall (_ _ : SRep), SRep
+  := let v := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)) in
+     v.
+Definition SRepAdd' : forall (_ _ : SRep), SRep
+  := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)).
+(* Error:
+In environment
+x : SRep
+y : SRep
+The term "x" has type "SRep" while it is expected to have type
+ "@LargeT ?e ?ZLikeOps".
+ *)
diff --git a/test-suite/bugs/closed/5203.v b/test-suite/bugs/closed/5203.v
new file mode 100644
index 000000000..ed137395f
--- /dev/null
+++ b/test-suite/bugs/closed/5203.v
@@ -0,0 +1,5 @@
+Goal True.
+  Typeclasses eauto := debug.
+  Fail solve [ typeclasses eauto ].
+  Fail typeclasses eauto.
+  
\ No newline at end of file
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 5557ba837..f62427ef4 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,15 +1,28 @@
 Module onlyclasses.
 
+(* In 8.6 we still allow non-class subgoals *)
   Variable Foo : Type.
   Variable foo : Foo.
   Hint Extern 0 Foo => exact foo : typeclass_instances.
   Goal Foo * Foo.
     split. shelve.
     Set Typeclasses Debug.
-    Fail (unshelve typeclasses eauto); fail.
-    typeclasses eauto with typeclass_instances.
-    Unshelve. typeclasses eauto with typeclass_instances.
+    typeclasses eauto.
+    Unshelve. typeclasses eauto.
   Qed.
+
+  Module RJung.
+    Class Foo (x : nat).
+      
+      Instance foo x : x = 2 -> Foo x.
+      Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.
+      Typeclasses eauto := debug.
+      Check (_ : Foo 2).
+
+
+      Fail Definition foo := (_ : 0 = 0).
+
+  End RJung.
 End onlyclasses.
 
 Module shelve_non_class_subgoals.
@@ -17,16 +30,36 @@ Module shelve_non_class_subgoals.
   Variable foo : Foo.
   Hint Extern 0 Foo => exact foo : typeclass_instances.
   Class Bar := {}.
-  Instance bar1 (f:Foo) : Bar.
+  Instance bar1 (f:Foo) : Bar := {}.
 
   Typeclasses eauto := debug.
   Set Typeclasses Debug Verbosity 2.
   Goal Bar.
     (* Solution has shelved subgoals (of non typeclass type) *)
-    Fail typeclasses eauto.
+    typeclasses eauto.
   Abort.
 End shelve_non_class_subgoals.
 
+Module RefineVsNoTceauto.
+
+  Class Foo (A : Type) := foo : A.
+  Instance: Foo nat := { foo := 0 }.
+  Instance: Foo nat := { foo := 42 }.
+  Hint Extern 0 (_ = _) => refine eq_refl : typeclass_instances.
+  Goal exists (f : Foo nat), @foo _ f = 0.
+  Proof.
+    unshelve (notypeclasses refine (ex_intro _ _ _)). 
+    Set Typeclasses Debug. Set Printing All.
+    all:once (typeclasses eauto).
+    Fail idtac. (* Check no subgoals are left *)
+    Undo 3.
+    (** In this case, the (_ = _) subgoal is not considered 
+        by typeclass resolution *)
+    refine (ex_intro _ _ _). Fail reflexivity.
+  Abort.
+
+End RefineVsNoTceauto.
+
 Module Leivantex2PR339.
   (** Was a bug preventing to find hints associated with no pattern *)
   Class Bar := {}.
@@ -34,8 +67,9 @@ Module Leivantex2PR339.
   Hint Extern 0 => exact True : typeclass_instances.
   Typeclasses eauto := debug.
   Goal Bar.
-    Fail typeclasses eauto.
     Set Typeclasses Debug Verbosity 2.
+    typeclasses eauto. (* Relies on resolution of a non-class subgoal *)
+    Undo 1.
     typeclasses eauto with typeclass_instances.
   Qed.
 End Leivantex2PR339.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 0af367781..3178c6fc1 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:[> (unshelve typeclasses eauto; fail) + reflexivity .. ].
+    all:[> typeclasses eauto + reflexivity .. ].
     Undo 1.
-    all:((unshelve typeclasses eauto; fail) + reflexivity). (* Note "+" is a focussing combinator *)
+    all:(typeclasses eauto + 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:((unshelve typeclasses eauto; fail) + reflexivity).
+      all:(typeclasses eauto + reflexivity).
     Qed.      
   End Leivant.
 End Backtracking.