diff options
| author | filliatr | 2003-01-20 09:28:23 +0000 |
|---|---|---|
| committer | filliatr | 2003-01-20 09:28:23 +0000 |
| commit | dc56ef6176581f6a66e5692bf350e1ed9fe806ba (patch) | |
| tree | b0f9ced18b7d66384a5a48d70099df28d1d4d91f | |
| parent | 6c48a70958815147a13d01fc4e1739329490a0fe (diff) | |
deplacement du test 'il reste des preuves en cours'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3544 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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") |