1 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v
new file mode 100644
index 00000000..9e6107b3
--- /dev/null
+++ b/test-suite/bugs/opened/3459.v
@@ -0,0 +1,31 @@
+(* Bad interaction between clear and the typability of ltac constr bindings *)
+
+(* Original report *)
+
+Goal 1 = 2.
+Proof.
+(* This line used to fail with a Not_found up to some point, and then
+   to produce an ill-typed term *)
+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.
+(* Add extra test for typability (should not fail when bug closed) *)
+Fail match goal with P:?c |- _ => try (let x := type of c in idtac) || fail 2 end.
+Abort.
+
+(* Second report raising a Not_found at the time of 21 Oct 2014 *)
+
+Section F.
+
+Variable x : nat.
+
+Goal True.
+evar (e : Prop).
+assert e.
+Fail let r := constr:(eq_refl x) in clear x; exact r.
+Abort.
+
+End F.