aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorLocation_12774_2.v
blob: e50e1caa0ffc53ec6e42742f49db8bd67ed540fe (plain)
1
2
3
4
Ltac f := simpl.
Goal Type.
f; exact 0.
Abort.