blob: e396fe06e52ad12bf8416510c604a7e79fc1bc6e (
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 : appcontext G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H'
end
in pose H.
|
