blob: 9e6107b30a407fff4d2d65aaff9cce8e1f1508f9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
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.
|
