Remove almost all the uses of string concatenation when building error messages.

Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.

4 files changed, 16 insertions, 17 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f8264e5af6..a669aef9a8 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1260,13 +1260,12 @@ module Make
 
         and pr_tacarg = function
           | TacDynamic (loc,t) ->
-            pr_with_comments loc (
-              str "<" ++ keyword "dynamic" ++ str (" [" ^ (Dyn.tag t)^"]>")
-            )
+            pr_with_comments loc
+              (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
           | MetaIdArg (loc,true,s) ->
-            pr_with_comments loc (str ("$" ^ s))
+            pr_with_comments loc (str "$" ++ str s)
           | MetaIdArg (loc,false,s) ->
-            pr_with_comments loc (keyword "constr:" ++ str(" $" ^ s))
+            pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s)
           | Reference r ->
             pr.pr_reference r
           | ConstrMayEval c ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 89ffae4b3e..c6b1b672f8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1253,7 +1253,7 @@ module Make
     and pr_extend s cl =
       let pr_arg a =
         try pr_gen a
-        with Failure _ -> str ("<error in "^fst s^">") in
+        with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
       try
         let rl = Egramml.get_extend_vernac_rule s in
         let start,rl,cl =
@@ -1271,7 +1271,7 @@ module Make
             (start,cl) rl in
         hov 1 pp
       with Not_found ->
-        hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+        hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
     in pr_vernac
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 4a66c33df8..e50435cda2 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -180,16 +180,16 @@ let print_opacity ref =
     | None -> []
     | Some s ->
        [pr_global ref ++ str " is " ++
-        str (match s with
-          | FullyOpaque -> "opaque"
+        match s with
+          | FullyOpaque -> str "opaque"
           | TransparentMaybeOpacified Conv_oracle.Opaque ->
-              "basically transparent but considered opaque for reduction"
+              str "basically transparent but considered opaque for reduction"
           | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev ->
-              "transparent"
+              str "transparent"
           | TransparentMaybeOpacified (Conv_oracle.Level n) ->
-              "transparent (with expansion weight "^string_of_int n^")"
+              str "transparent (with expansion weight " ++ int n ++ str ")"
           | TransparentMaybeOpacified Conv_oracle.Expand ->
-              "transparent (with minimal expansion weight)")]
+              str "transparent (with minimal expansion weight)"]
 
 (*******************)
 (* *)
@@ -386,9 +386,9 @@ let print_located_qualid name flags ref =
     | [] ->
 	let (dir,id) = repr_qualid qid in
 	if DirPath.is_empty dir then
-	  str ("No " ^ name ^ " of basename") ++ spc () ++ pr_id id
+	  str "No " ++ str name ++ str " of basename" ++ spc () ++ pr_id id
 	else
-	  str ("No " ^ name ^ " of suffix") ++ spc () ++ pr_qualid qid
+	  str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid
     | l ->
 	prlist_with_sep fnl
 	(fun (o,oqid) ->
diff --git a/printing/printer.ml b/printing/printer.ml
index 0d3a1c17e4..141ae145dd 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -654,7 +654,7 @@ let pr_goal_by_id id =
   let p = Proof_global.give_me_the_proof () in
   let g = Goal.get_by_uid id in
   let pr gs =
-    v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut ()
+    v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut ()
 	 ++ pr_goal gs)
   in
   try
@@ -723,7 +723,7 @@ let pr_assumptionset env s =
       try pr_constant env kn
       with Not_found ->
 	let mp,_,lab = repr_con kn in
-	str (string_of_mp mp ^ "." ^ Label.to_string lab)
+        str (string_of_mp mp) ++ str "." ++ pr_label lab
     in
     let safe_pr_ltype typ =
       try str " : " ++ pr_ltype typ