aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_9114.v
blob: 2cf91c1c2b0a9810d194eae6c3440c50cb0a9617 (plain)
1
2
3
4
5
Goal True.
  assert_succeeds (exact I).
  idtac.
  (* Error: No such goal. *)
Abort.