theorem.v « coqwc « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/coqwc/theorem.v

blob: 901c9074fdfaf264cb82677985289c0c9ff5344a (plain)

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