More precise test for #3459.

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v
index db42d9605..949cace1d 100644
--- a/test-suite/bugs/opened/3459.v
+++ b/test-suite/bugs/opened/3459.v
@@ -1,9 +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 *)
+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.
+let r := constr:(eq_refl x) in clear x; exact r.
+Abort.
+
+End F.