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

Was PR#381: V8.6+fix typeclasses eauto shelving

2 files changed, 11 insertions, 10 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e44ace4257..b416bc657a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1124,12 +1124,12 @@ module Search = struct
           else tclDISPATCH
                  (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j))))
         in
-        let finish sigma =
+        let finish nestedshelf sigma =
           let filter ev =
             try
               let evi = Evd.find_undefined sigma ev in
               if info.search_only_classes then
-                Some (ev, is_class_type sigma (Evd.evar_concl evi))
+                Some (ev, not (is_class_type sigma (Evd.evar_concl evi)))
               else Some (ev, true)
             with Not_found -> None
           in
@@ -1147,9 +1147,9 @@ module Search = struct
           begin
             (* Some existentials produced by the original tactic were not solved
                in the subgoals, turn them into subgoals now. *)
-            let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in
-            let shelved = List.map fst shelved and goals = List.map fst goals in
-            if !typeclasses_debug > 1 && not (List.is_empty goals) then
+            let shelved, goals = List.partition (fun (ev, s) -> s) remaining in
+            let shelved = List.map fst shelved @ nestedshelf and goals = List.map fst goals in
+            if !typeclasses_debug > 1 && not (List.is_empty shelved && List.is_empty goals) then
               Feedback.msg_debug
                 (str"Adding shelved subgoals to the search: " ++
                  prlist_with_sep spc (pr_ev sigma) goals ++
@@ -1162,7 +1162,8 @@ module Search = struct
 	         with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>=
                       fun s -> result s i (Some (Option.default 0 k + j)))
           end
-        in res <*> tclEVARMAP >>= finish
+        in with_shelf res >>= fun (sh, ()) ->
+           tclEVARMAP >>= finish sh
       in
       if path_matches derivs [] then aux e tl
       else
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index f62427ef47..6b1f0315bc 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -98,7 +98,7 @@ Goal exists R, @Refl nat R.
   solve [typeclasses eauto with foo].
 Qed.
 
-(* Set Typeclasses Compatibility "8.5". *)
+Set Typeclasses Compatibility "8.5".
 Parameter f : nat -> Prop.
 Parameter g : nat -> nat -> Prop.
 Parameter h : nat -> nat -> nat -> Prop.
@@ -108,8 +108,7 @@ Axiom c : forall x y z, h x y z -> f x -> f y.
 Hint Resolve a b c : mybase.
 Goal forall x y z, h x y z -> f x -> f y.
   intros.
-  Set Typeclasses Debug.
-  typeclasses eauto with mybase.
+  Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *)
   Unshelve.
 Abort.
 End bt.
@@ -138,7 +137,8 @@ Notation "'return' t" := (unit t).
 Class A `(e: T) := { a := True }.
 Class B `(e_: T) := { e := e_; sg_ass :> A e }.
 
-Set Typeclasses Debug.
+(* Set Typeclasses Debug. *)
+(* Set Typeclasses Debug Verbosity 2. *)
 
 Goal forall `{B T}, Prop.
   intros. apply a.