1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3459.v b/test-suite/bugs/closed/3459.v
new file mode 100644
index 000000000..db42d9605
--- /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.