From c28a2a3a1297098ee73ad5b26e714164b6167d2b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 21 Oct 2016 18:39:05 +0200
Subject: Adding a test for bug #3495.

---
 test-suite/bugs/closed/3495.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/bugs/closed/3495.v

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.
-- 
cgit v1.2.3