diff options
| -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 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(); |