From 1b995f87ea992092acc7990039b343f5afacd296 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Sep 2014 14:12:39 +0200
Subject: Test for bug #3459.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3459.v b/test-suite/bugs/closed/3459.v
new file mode 100644
index 0000000000..db42d96053
--- /dev/null
+++ b/test-suite/bugs/closed/3459.v
@@ -0,0 +1,9 @@
+Goal 1 = 2.
+Proof.
+match goal with
+  | [ |- context G[2] ] => let y := constr:(fun x => $(let r := constr:(@eq Set x x) in
+                                                       clear x;
+                                                       exact r)$) in
+                           pose y
+end.
+Abort.
-- 
cgit v1.2.3