blob: e727e26061931cab098d79455acfb2e6afb57215 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* 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.
|
