aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorLocation_12152_1.v
blob: 709ac305e41906c2de88f5374efae55ee43f642a (plain)
1
2
3
4
(* Reported in #12152 *)
Goal True.
intro H; auto.
Abort.