diff options
| author | Emilio Jesus Gallego Arias | 2016-12-07 12:12:54 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:51:42 +0100 |
| commit | 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 (patch) | |
| tree | 562c3470d8d2f02226ccf27d032a64a5e9a5dc17 /proofs | |
| parent | 3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 (diff) | |
[pp] [ide] Minor cleanups in pp code.
- We avoid unnecessary use of Pp -> string conversion functions.
and the creation of intermediate buffers on logging.
- We rename local functions that share the name with the Coq stdlib,
this is usually dangerous as if the normal function is removed, code
may pick up the one in the stdlib, with different semantics.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 4 | ||||
| -rw-r--r-- | proofs/proof_using.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 120cde5e55..ca7330fdb6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -195,9 +195,9 @@ let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - CErrors.error (Pp.string_of_ppcmds + CErrors.user_err (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++ - str"Use \"Abort All\" first or complete proof(s).")) + str"Use \"Abort All\" first or complete proof(s).") end let discard_gen id = diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index a125fb10db..f51586c739 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids = let suggest_Proof_using name env vars ids_typ context_ids = let module S = Id.Set in let open Pp in - let print x = prerr_endline (string_of_ppcmds x) in + let print x = Feedback.msg_error x in let pr_set parens s = let wrap ppcmds = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" |