Adding a test for bug #3495.

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3495.v b/test-suite/bugs/closed/3495.v
new file mode 100644
index 0000000000..102a2aba0d
--- /dev/null
+++ b/test-suite/bugs/closed/3495.v
@@ -0,0 +1,18 @@
+Require Import RelationClasses.
+
+Axiom R : Prop -> Prop -> Prop.
+Declare Instance : Reflexive R.
+
+Class bar := { x : False }.
+Record foo := { a : Prop ; b : bar }.
+
+Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}.
+
+Goal exists k, R k True.
+Proof.
+eexists.
+evar (b : bar).
+let e := match goal with |- R ?e _ => constr:(e) end in
+unify e (a (default_foo True)).
+subst b.
+reflexivity.