diff options
| -rw-r--r-- | toplevel/coqtop.ml | 8 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 |
2 files changed, 5 insertions, 7 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ce6f6af03b..2df94d133c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -244,13 +244,9 @@ let start () = msgnl (Toplevel.print_toplevel_error e); exit 1 end; - if !batch_mode then - if Pfedit.get_all_proof_names () = [] then - (flush_all(); Profile.print_profile ();exit 0) - else - (message "Error: There are pending proofs"; exit 1); + if !batch_mode then (flush_all(); Profile.print_profile (); exit 0); Toplevel.loop(); -(* Initialise and launch the Ocaml toplevel *) + (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); exit 1 diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 5dba3cdec8..2f6d5c934e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -179,4 +179,6 @@ let compile verbosely f = let ldir,long_f_dot_v = Library.start_library f in if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); let _ = load_vernac verbosely long_f_dot_v in - Library.save_library_to ldir (long_f_dot_v^"o") + if Pfedit.get_all_proof_names () <> [] then + (message "Error: There are pending proofs"; exit 1); + Library.save_library_to ldir (long_f_dot_v ^ "o") |