diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-15 20:01:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-15 20:01:28 +0100 |
| commit | 7d2282bc2b9258c5b7d575ada1292a2a06ad0544 (patch) | |
| tree | 716eb26fa7a541d024481daacd98085aa6152516 /toplevel | |
| parent | d549e018fd5d4a9429025399885ed04d40b5de97 (diff) | |
Removing a pperrnl.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 2edc9759e..98a3d7496 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -308,7 +308,7 @@ let compile verbosely f = let check_pending_proofs () = let pfs = Pfedit.get_all_proof_names () in if not (List.is_empty pfs) then - (pperrnl (str "Error: There are pending proofs"); flush_all (); exit 1) in + (msg_error (str "There are pending proofs"); flush_all (); exit 1) in match !Flags.compilation_mode with | BuildVo -> let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in |