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

about summary refs log tree commit diff homepage

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

blob: e69e23276b447638e7220f243af4e0e08f8527ea (plain)

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