diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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(); |