diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 0f3fed704..99552c552 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -179,10 +179,9 @@ let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - pp_with Format.str_formatter + Util.error (Pp.string_of_ppcmds (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++ - str"Use \"Abort All\" first or complete proof(s).") ; - Util.error (Format.flush_str_formatter ()) + str"Use \"Abort All\" first or complete proof(s).")) end |