Fix iterative deepening strategy failing too early

Report limit exceeded on _any_ branch so that we pursue search
if it was reached at least once. Add example by N. Tabareau in
test-suite.

2 files changed, 51 insertions, 8 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3c2ef406ee..fea8189eb6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -555,6 +555,12 @@ let needs_backtrack' env evd unique concl =
     occur_existential concl
   else true
 
+let merge_exceptions e e' =
+  match fst e, fst e' with
+  | ReachedLimitEx, _ -> e
+  | _, ReachedLimitEx -> e'
+  | _, _ -> e
+
 let new_hints_tac_gl only_classes hints info kont gl
     : unit Proofview.tactic
  =
@@ -615,7 +621,8 @@ let new_hints_tac_gl only_classes hints info kont gl
            else Proofview.tclDISPATCH (List.init j (tac_of i)))
        in
        if path_matches derivs [] then aux foundone e tl
-       else ortac (Proofview.tclBIND tac result) (fun e -> aux foundone e tl)
+       else ortac (Proofview.tclBIND tac result)
+                  (fun e' -> aux foundone (merge_exceptions e e') tl)
     | [] ->
        if foundone == None && !typeclasses_debug then
 	 msg_debug (pr_depth info.search_depth ++ str": no match for " ++
@@ -624,7 +631,7 @@ let new_hints_tac_gl only_classes hints info kont gl
                       str" possibilities");
        match e with
        | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx
-       | _ -> Tacticals.New.tclFAIL 0 (str"no hint applies")
+       | (_,ie) -> Proofview.tclZERO ~info:ie NotApplicableEx
   in aux None (NotApplicableEx,Exninfo.null) poss
 
 let new_hints_tac cl hints info kont : unit Proofview.tactic =
@@ -659,12 +666,6 @@ let intro_tac' only_classes info kont =
    (fun _ ->
      Proofview.Goal.nf_enter { enter = fun gl -> intro_tac'' only_classes info kont gl })
 
-let merge_exceptions e e' =
-  match fst e, fst e' with
-  | ReachedLimitEx, _ -> e
-  | _, ReachedLimitEx -> e'
-  | _, _ -> e
-
 let rec eauto_tac' only_classes hints limit depth =
   let kont info =
     Proofview.numgoals >>= fun i ->
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 837d9d4c17..26a4c4d916 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -121,3 +121,45 @@ Lemma simpl_plus_l_rr1 :
   Undo.
   eauto. (* does EApply H *)
 Qed.
+
+(* Example from Nicolas Tabareau on coq-club - Feb 2016. 
+  Full backtracking on dependent subgoals.
+ *)
+Require Import Coq.Classes.Init.
+Set Typeclasses Dependency Order.
+Unset Typeclasses Iterative Deepening.
+Notation "x .1" := (projT1 x) (at level 3).
+Notation "x .2" := (projT2 x) (at level 3).
+
+Parameter myType: Type. 
+
+Class Foo (a:myType) := {}.
+
+Class Bar (a:myType) := {}.
+
+Class Qux (a:myType) := {}.
+
+Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}.
+
+Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}.
+
+Hint Extern 5 (Bar ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 5 (Qux ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 1 myType => unshelve refine (fooTobar _ _).1 : typeclass_instances.
+
+Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances.
+
+Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instances.
+
+Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
+Proof.
+  Fail typeclasses eauto with typeclass_instances.
+  fulleauto 4.
+  Undo. Set Typeclasses Iterative Deepening.
+  fulleauto.
+Defined.
+