1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v
new file mode 100644
index 00000000..1e47f295
--- /dev/null
+++ b/test-suite/bugs/closed/4863.v
@@ -0,0 +1,33 @@
+Require Import Classes.DecidableClass.
+
+Inductive Foo : Set :=
+| foo1 | foo2.
+
+Lemma 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 (Decidable (?A = ?B)) => abstract (abstract (abstract (apply Decidable_sumbool; 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*)