Theorem foo : True.
Proof.
  idtac. (* comment *)
  idtac.
  idtac.
  idtac. (* comment *)
  idtac.
  idtac.
  auto.
Qed.