diff options
Diffstat (limited to 'test-suite/success/Typeclasses.v')
-rw-r--r-- | test-suite/success/Typeclasses.v | 23 |
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. |