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.

2 files changed, 78 insertions, 0 deletions

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index f25e18acd..8d6cbfcde 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,41 @@
+Module bt.
+Require Import Equivalence.
+
+Record Equ (A : Type) (R : A -> A -> Prop).
+Definition equiv {A} R (e : Equ A R) := R.
+Record Refl (A : Type) (R : A -> A -> Prop).
+Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e).
+Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [|shelve|] : foo.
+
+Variable R : nat -> nat -> Prop.
+Lemma bas : Equ nat R.
+Admitted.
+Hint Resolve bas : foo.
+Hint Extern 1 => match goal with |- (_ -> _ -> Prop) => shelve end : foo.
+
+Goal exists R, @Refl nat R.
+  eexists.
+  Set Typeclasses Debug.
+  (* Fail solve [unshelve eauto with foo]. *)
+  Set Typeclasses Debug Verbosity 1.
+  solve [typeclasses eauto with foo].
+Qed.
+
+(* Set Typeclasses Compatibility "8.5". *)
+Parameter f : nat -> Prop.
+Parameter g : nat -> nat -> Prop.
+Parameter h : nat -> nat -> nat -> Prop.
+Axiom a : forall x y, g x y -> f x -> f y.
+Axiom b : forall x (y : Empty_set), g (fst (x,y)) x.
+Axiom c : forall x y z, h x y z -> f x -> f y.
+Hint Resolve a b c : mybase.
+Goal forall x y z, h x y z -> f x -> f y.
+  intros.
+  Set Typeclasses Debug.
+  typeclasses eauto with mybase.
+  Unshelve.
+Abort.
+End bt.
 Generalizable All Variables.
 
 Module mon.
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.