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

2 files changed, 5 insertions, 0 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 7b21f9bbd9..80c599274a 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -77,6 +77,8 @@ let app s1 s2 = match s1, s2 with
   | s, Ppcmd_empty -> s
   | s1, s2         -> Ppcmd_glue [s1; s2]
 
+let seq s = Ppcmd_glue s
+
 let (++) = app
 
 (* formatting commands *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 2c45ce0a70..4b7ac5c1ae 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -68,6 +68,9 @@ val comment  : string list -> std_ppcmds
 val app : std_ppcmds -> std_ppcmds -> std_ppcmds
 (** Concatenation. *)
 
+val seq : std_ppcmds list -> std_ppcmds
+(** Multi-Concatenation. *)
+
 val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
 (** Infix alias for [app]. *)