From dc56ef6176581f6a66e5692bf350e1ed9fe806ba Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 20 Jan 2003 09:28:23 +0000
Subject: 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
---
 toplevel/coqtop.ml | 8 ++------
 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")
-- 
cgit v1.2.3