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.

4 files changed, 87 insertions, 9 deletions

diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v
new file mode 100644
index 0000000000..7254afb429
--- /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 0000000000..ed137395fc
--- /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 5557ba8379..f62427ef47 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 0af367781a..3178c6fc15 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.