aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorLocation_12152_2.v
blob: 5df6bec939a41d6bd958461c3c9bcfac706fb4d4 (plain)
1
2
3
(* Reported in #12152 *)
Goal True.
intros H; auto.