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, 29 insertions, 23 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index c8cb1d1cc..9b358210a 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -12,6 +12,7 @@ open Names
 open Evd
 open Evarutil
 open Evarsolve
+open Pp
 
 (******************************************)
 (* Instantiation of existential variables *)
@@ -54,8 +55,8 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     with e when Errors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err_loc
-        (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
-			string_of_existential evk))
+        (loc,"", str "Instance is not well-typed in the environment of " ++
+                 str (string_of_existential evk))
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b8206ca1b..898588d9e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -179,7 +179,8 @@ let check_decl_position env sign (x,_,_ as d) =
   let needed = global_vars_set_of_decl env d in
   let deps = dependency_closure env (named_context_of_val sign) needed in
   if Id.List.mem x deps then
-    error ("Cannot create self-referring hypothesis "^Id.to_string x);
+    errorlabstrm "Logic.check_decl_position"
+      (str "Cannot create self-referring hypothesis " ++ pr_id x);
   x::deps
 
 (* Auxiliary functions for primitive MOVE tactic
@@ -488,9 +489,11 @@ let convert_hyp check sign sigma (id,b,bt as d) =
       (fun _ (_,c,ct) _ ->
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma bt ct) then
-	  error ("Incorrect change of the type of "^(Id.to_string id)^".");
+	  errorlabstrm "Logic.convert_hyp"
+            (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
-	  error ("Incorrect change of the body of "^(Id.to_string id)^".");
+	  errorlabstrm "Logic.convert_hyp"
+            (str "Incorrect change of the body of "++ pr_id id ++ str ".");
        if check then reorder := check_decl_position env sign d;
        d) in
   reorder_val_context env sign' !reorder
@@ -522,7 +525,8 @@ let prim_refiner r sigma goal =
 	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
-	      error ("Variable " ^ Id.to_string id ^ " is already declared.");
+	      errorlabstrm "Logic.prim_refiner"
+                (str "Variable " ++ pr_id id ++ str " is already declared.");
 	     push_named_context_val (id,None,t) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
@@ -550,11 +554,10 @@ let prim_refiner r sigma goal =
 	  | (f,n,ar)::oth ->
 	      let ((sp',_),u')  = check_ind env n ar in
 	      if not (eq_mind sp sp') then
-		error ("Fixpoints should be on the same " ^
-		       "mutual inductive declaration.");
+		error "Fixpoints should be on the same mutual inductive declaration.";
 	      if !check && mem_named_context f (named_context_of_val sign) then
-		error
-		  ("Name "^Id.to_string f^" already used in the environment");
+		errorlabstrm "Logic.prim_refiner"
+		  (str "Name " ++ pr_id f ++ str " already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] ->
 	      Evd.Monad.List.map (fun (_,_,c) sigma ->
@@ -584,8 +587,7 @@ let prim_refiner r sigma goal =
 		try
 		  let _ = find_coinductive env sigma b in ()
                 with Not_found ->
-		  error ("All methods must construct elements " ^
-			  "in coinductive types.")
+		  error "All methods must construct elements in coinductive types."
 	in
 	let firsts,lasts = List.chop j others in
 	let all = firsts@(f,cl)::lasts in
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 1383d7556..d25f7e915 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -167,18 +167,20 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
 
 let declare_reduction s f =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then error ("There is already a reduction expression of name "^s)
+  then errorlabstrm "Redexpr.declare_reduction"
+    (str "There is already a reduction expression of name " ++ str s)
   else reduction_tab := String.Map.add s f !reduction_tab
 
 let check_custom = function
   | ExtraRedExpr s ->
       if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
-      then error ("Reference to undefined reduction expression "^s)
+      then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
   |_ -> ()
 
 let decl_red_expr s e =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then error ("There is already a reduction expression of name "^s)
+  then errorlabstrm "Redexpr.decl_red_expr"
+    (str "There is already a reduction expression of name " ++ str s)
   else begin
     check_custom e;
     red_expr_tab := String.Map.add s e !red_expr_tab
@@ -232,7 +234,8 @@ let reduction_of_red_expr env =
       with Not_found ->
 	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
 	 with Not_found ->
-	   error("unknown user-defined reduction \""^s^"\"")))
+	   errorlabstrm "Redexpr.reduction_of_red_expr"
+             (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
   | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
   in
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 3cc81daf5..d7f4b5ead 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -11,6 +11,7 @@ open Names
 open Pp
 open Tacexpr
 open Termops
+open Nameops
 
 let (prtac, tactic_printer) = Hook.make ()
 let (prmatchpatt, match_pattern_printer) = Hook.make ()
@@ -231,17 +232,16 @@ let db_pattern_rule debug num r =
 
 (* Prints the hypothesis pattern identifier if it exists *)
 let hyp_bound = function
-  | Anonymous -> " (unbound)"
-  | Name id -> " (bound to "^(Names.Id.to_string id)^")"
+  | Anonymous -> str " (unbound)"
+  | Name id -> str " (bound to " ++ pr_id id ++ str ")"
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,_,c) ido =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str "Hypothesis " ++
-           str ((Names.Id.to_string id)^(hyp_bound ido)^
-                " has been matched: ") ++ print_constr_env env c)
+    msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++
+                str " has been matched: " ++ print_constr_env env c)
   else return ()
 
 (* Prints the matched conclusion *)
@@ -266,8 +266,8 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^
-                " cannot match: ") ++
+    msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++
+                str " cannot match: " ++
            Hook.get prmatchpatt env sigma hyp)
   else return ()