test-suite/coqwc/next-obligation.v


1
2
3
4
5
6
7
8
9
10

(* make sure all proof lines are counted *)

Goal True. 
  Next Obligation.
  idtac.
  Next Obligation.
  idtac.
  Next Obligation.
  idtac.
Qed.