diff options
Diffstat (limited to 'test-suite/success/bteauto.v')
-rw-r--r-- | test-suite/success/bteauto.v | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v new file mode 100644 index 000000000..f55e32032 --- /dev/null +++ b/test-suite/success/bteauto.v @@ -0,0 +1,40 @@ + +Class A := { foo : nat }. + +Instance A_1 : A | 2 := { foo := 42 }. +Instance A_0 : A | 1 := { foo := 0 }. +Lemma aeq (a : A) : foo = foo. + reflexivity. +Qed. + +Goal exists n, n = 42. + eexists. + eapply eq_trans. + evar (a : A). subst a. + refine (@aeq ?a). + Unshelve. all:cycle 1. + typeclasses eauto. + Fail reflexivity. + Undo 2. + Set Typeclasses Debug. + (* Without multiple successes it fails *) + Fail all:((once typeclasses eauto) + reflexivity). + (* Does backtrack if other goals fail *) + all:((typeclasses eauto) + reflexivity). +Qed. + +Hint Extern 0 (_ = _) => reflexivity : typeclass_instances. + +Goal exists n, n = 42. + eexists. + eapply eq_trans. + evar (a : A). subst a. + refine (@aeq ?a). + Unshelve. all:cycle 1. + typeclasses eauto. + Fail reflexivity. + Undo 2. + Set Typeclasses Debug. + (* Does backtrack between individual goals *) + all:(typeclasses eauto). +Qed. |