From ca30a8be08beeae77d42b6cb5d9f219e3932a3f7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 17:12:39 -0500
Subject: Fix bug #3257, setoid_reflexivity should fail if not completing the
 goal.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3257.v b/test-suite/bugs/closed/3257.v
new file mode 100644
index 0000000000..d8aa6a0479
--- /dev/null
+++ b/test-suite/bugs/closed/3257.v
@@ -0,0 +1,5 @@
+Require Import Setoid Morphisms Basics.
+Lemma foo A B (P : B -> Prop) :
+  pointwise_relation _ impl (fun z => A -> P z) P.
+Proof.
+  Fail reflexivity.
-- 
cgit v1.2.3