From c4aa6b21f558415f3bea3e5f872d3e6cb90c1f72 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 17 Jan 2003 16:58:01 +0000
Subject: msg Failtac; echec -batch s'il reste des preuves

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3525 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/cerrors.ml | 3 +--
 toplevel/coqtop.ml  | 6 +++++-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index b2154c74d7..129794c587 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -85,8 +85,7 @@ let rec explain_exn_default = function
       hov 0 (str "Error:" ++ spc () ++
 	       str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q)
   | Refiner.FailError i ->
-      hov 0 (str "Error: Fail tactic always fails (level " ++ 
-	       int i ++ str").")
+      hov 0 (str "Error: Tactic failed (level " ++ int i ++ str").")
   | Stdpp.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a23ba7335c..ce6f6af03b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -244,7 +244,11 @@ let start () =
       msgnl (Toplevel.print_toplevel_error e);
       exit 1
   end;
-  if !batch_mode then (flush_all(); Profile.print_profile ();exit 0);
+  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);
   Toplevel.loop();
 (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();
-- 
cgit v1.2.3