blob: 7388555a1f41e0828a4802e73b7ea8a836ebc4f1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* Check a case where ltac typing error should result in error, not anomaly *)
Goal forall (H : forall x : nat, x = x), False.
intro.
Fail
let H :=
match goal with
| [ H : context G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H'
end
in pose H.
Abort.
|
