bteauto: a Proofview.tactic for multiple goals

Add an option to force backtracking at toplevel, which
is used by default when calling typeclasses eauto on a set of goals.
They might be depended on by other subgoals, so the tactic should
be backtracking by default, a once can make it not backtrack.

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.