Merge remote-tracking branch 'github/bug4863' into v8.5

1 files changed, 32 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v
new file mode 100644
index 0000000000..e884355fde
--- /dev/null
+++ b/test-suite/bugs/closed/4863.v
@@ -0,0 +1,32 @@
+Require Import Classes.DecidableClass.
+
+Inductive Foo : Set :=
+| foo1 | foo2.
+
+Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
+Proof.
+  intros P H.
+  refine (Build_Decidable _ (if H then true else false) _).
+  intuition congruence.
+Qed.
+
+Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances.
+
+Goal forall (a b : Foo), {a=b}+{a<>b}.
+intros.
+abstract (abstract (decide equality)). (*abstract works here*)
+Qed.
+
+Check ltac:(abstract (exact I)) : True.
+
+Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
+intros.
+split. typeclasses eauto. typeclasses eauto. Qed.
+
+Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
+intros.
+split.
+refine _.
+refine _.
+Defined.
+(*fails*)