[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.

1 files changed, 1 insertions, 1 deletions

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 ")"