Merge remote-tracking branch 'github/pr/362' into v8.6

Was PR#362: Revert another part of a477dc in good measure

6 files changed, 102 insertions, 24 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 7c4bd4d201..bd8ee450ef 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 99a1a98993..e44ace4257 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
@@ -1317,10 +1318,9 @@ module Search = struct
        Feedback.msg_debug (str"Starting resolution with " ++ int i ++
                              str" goal(s) under focus and " ++
                              int (List.length initshelf) ++ str " shelved goal(s)" ++
-                             if only_classes then str " in only_classes mode" else
-                               str " in regular mode" ++
-                                 match depth with None -> str ", unbounded"
-                                                | Some i -> str ", with depth limit " ++ int i));
+                             (if only_classes then str " in only_classes mode" else str " in regular mode") ++
+                             match depth with None -> str ", unbounded"
+                                            | Some i -> str ", with depth limit " ++ int i));
     tac
 
   let run_on_evars p evm tac =
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.