aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorLocation_12774_3.v
blob: c624402a81465ec606da2d0cd148806f332c0bc2 (plain)
1
2
3
4
Ltac f := auto; intro.
Goal False.
f.
Abort.