diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-17 16:58:01 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-17 16:58:01 +0000 |
| commit | c4aa6b21f558415f3bea3e5f872d3e6cb90c1f72 (patch) | |
| tree | 98a73da6094270ba565603fe76f708374bf6690d /toplevel | |
| parent | 3d31870b812eb8946354c359d5c1f63d1294f396 (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 6 |
2 files changed, 6 insertions, 3 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index b2154c74d..129794c58 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 a23ba7335..ce6f6af03 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(); |