Add an Iterative Deepening search strategy to typeclass resolution.

1 files changed, 22 insertions, 1 deletions

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 30a2a7429..d6e590af3 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -57,4 +57,25 @@ Section sec.
  let's try to get rid of the intermediate constant foo.
  Surely we can just expand it inline, right? Wrong!: *)
  Check U (fun x => e x) _.
-End sec.
\ No newline at end of file
+End sec.
+
+Module IterativeDeepening.
+
+  Class A.
+  Class B.
+  Class C.
+
+  Instance: B -> A | 0.
+  Instance: C -> A | 0.
+  Instance: C -> B -> A | 0.
+  Instance: A -> A | 0.
+  
+  Goal C -> A.
+    intros.
+    Set Typeclasses Debug.
+    Fail Timeout 1 typeclasses eauto.
+    Set Typeclasses Iterative Deepening.
+    typeclasses eauto.
+  Qed.
+
+End IterativeDeepening.