ErrorInSection.v « output « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/output/ErrorInSection.v

blob: 3036f8f05b79a9fc66c19376634d12c35dcc8c3f (plain)

(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
Section S.
  Definition foo := nonexistent.
End S.