[pp] Remove uses of expensive string_of_ppcmds.

In general we want to avoid this as much as we can, as it will need to
make choices regarding the output backend (width, etc...) and it is
expensive. It is better to serve the printing backends the pretty
print document itself.

3 files changed, 6 insertions, 5 deletions

diff --git a/vernac/search.ml b/vernac/search.ml
index e1b56b1319..540573843e 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -367,7 +367,7 @@ let interface_search =
     let answer = {
       coq_object_prefix = prefix;
       coq_object_qualid = qualid;
-      coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr);
+      coq_object_object = constr;
     } in
     ans := answer :: !ans;
   in
diff --git a/vernac/search.mli b/vernac/search.mli
index c9167c485d..82b79f75de 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -67,7 +67,7 @@ type 'a coq_object = {
 }
 
 val interface_search : ?glnum:int -> (search_constraint * bool) list ->
-  string coq_object list
+  constr coq_object list
 
 (** {6 Generic search function} *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 999fe297ed..32e18a0149 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -39,8 +39,9 @@ module NamedDecl = Context.Named.Declaration
 let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 
 let debug = false
-let vernac_prerr_endline x =
-  if debug then prerr_endline (x ()) else ()
+(* XXX Should move to a common library *)
+let vernac_pperr_endline pp =
+  if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else ()
 
 (* Misc *)
 
@@ -1933,7 +1934,7 @@ let vernac_load interp fname =
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~loc locality poly c =
-  vernac_prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
+  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
   match c with
   (* The below vernac are candidates for removal from the main type
      and to be put into a new doc_command datatype: *)