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.

8 files changed, 18 insertions, 16 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 048bd637aa..ad8164fa64 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -66,7 +66,7 @@ let find_base bas =
   try raw_find_base bas
   with Not_found ->
     errorlabstrm "AutoRewrite"
-      (str ("Rewriting base "^(bas)^" does not exist."))
+      (str "Rewriting base " ++ str bas ++ str " does not exist.")
 
 let find_rewrites bas =
   List.rev_map snd (HintDN.find_all (find_base bas))
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 816b54f027..5d6fcc5b10 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -306,8 +306,8 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	      let _ = Global.lookup_constant c1' in
 		c1'
 	    with Not_found -> 
-	      let rwr_thm = Label.to_string l' in 
-	      error ("Cannot find rewrite principle "^rwr_thm^".")
+	      errorlabstrm "Equality.find_elim"
+                (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
 	  end
 	| _ -> destConstRef pr1
         end
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 55d62e1514..f83aa56017 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -598,7 +598,7 @@ let current_pure_db () =
   List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
 
 let error_no_such_hint_database x =
-  error ("No such Hint database: "^x^".")
+  errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
 
 (**************************************************************************)
 (*                       Definition of the summary                        *)
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index ac8b4923e5..60ce0e0dc3 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -52,7 +52,7 @@ let try_find_global_reference dir s =
   let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
     try Nametab.global_of_path sp
     with Not_found -> 
-      anomaly (str ("Global reference " ^ s ^ " not found in generalized rewriting"))
+      anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting")
 
 let find_reference dir s =
   let gr = lazy (try_find_global_reference dir s) in
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 84c0a99b18..ffff44d5bc 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -43,7 +43,7 @@ end
 module MLTacMap = Map.Make(MLName)
 
 let pr_tacname t =
-  t.mltac_plugin ^ "::" ^ t.mltac_tactic
+  str t.mltac_plugin ++ str "::" ++ str t.mltac_tactic
 
 let tac_tab = ref MLTacMap.empty
 
@@ -52,9 +52,9 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
     if MLTacMap.mem s !tac_tab then
       if overwrite then
         let () = tac_tab := MLTacMap.remove s !tac_tab in
-        msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s))
+        msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s)
       else
-        Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ "."))
+        Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
   in
   tac_tab := MLTacMap.add s t !tac_tab
 
@@ -63,7 +63,7 @@ let interp_ml_tactic s =
     MLTacMap.find s !tac_tab
   with Not_found ->
     Errors.errorlabstrm ""
-      (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
+      (str "The tactic " ++ pr_tacname s ++ str " is not installed.")
 
 (***************************************************************************)
 (* Tactic registration *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0a746d283e..7ce158fd1a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1040,8 +1040,8 @@ let read_pattern lfun ist env sigma = function
 let cons_and_check_name id l =
   if Id.List.mem id l then
     user_err_loc (dloc,"read_match_goal_hyps",
-      strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^
-      " used twice in the same pattern."))
+      str "Hypothesis pattern-matching variable " ++ pr_id id ++
+      str " used twice in the same pattern.")
   else id::l
 
 let rec read_match_goal_hyps lfun ist env sigma lidh = function
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 17ac7a4b66..5ba53a7641 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -615,7 +615,8 @@ module New = struct
 	    | Var id -> string_of_id id
 	    | _ -> "\b"
 	  in
-	  error ("The elimination combinator " ^ name_elim ^ " is unknown.")
+	  errorlabstrm "Tacticals.general_elim_then_using"
+            (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain indmv elimclause indclause in
     let branchsigns = compute_construtor_signatures isrec ind in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b40c8d0e74..8117e4131b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -139,7 +139,8 @@ let introduction ?(check=true) id =
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
     let () = if check && mem_named_context id hyps then
-      error ("Variable " ^ Id.to_string id ^ " is already declared.")
+      errorlabstrm "Tactics.introduction"
+        (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
     match kind_of_term (whd_evar sigma concl) with
     | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b
@@ -1870,8 +1871,8 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if Int.equal i 0 then error "The constructors are numbered starting from 1.";
   begin match expctdnumopt with
     | Some n when not (Int.equal n nconstr) ->
-	error ("Not an inductive goal with "^
-	       string_of_int n ^ String.plural n " constructor"^".")
+	errorlabstrm "Tactics.check_number_of_constructors"
+          (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
     | _ -> ()
   end;
   if i > nconstr then error "Not enough constructors."
@@ -3042,7 +3043,7 @@ let make_up_names n ind_opt cname =
 
 let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
-  error ("Cannot recognize "^s^"an induction scheme.")
+  errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
 let glob = Universes.constr_of_global