From 16d301bab5b7dec53be4786b3b6815bca54ae539 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 23 Apr 2015 14:55:11 +0200
Subject: 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.
---
 interp/coqlib.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'interp/coqlib.ml')

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 02504c9202..5ac718e3b0 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -54,15 +54,15 @@ let gen_reference_in_modules locstr dirs s =
   match these with
     | [x] -> x
     | [] ->
-	anomaly ~label:locstr (str ("cannot find "^s^
-	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	anomaly ~label:locstr (str "cannot find " ++ str s ++
+	str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
 	prlist_with_sep pr_comma pr_dirpath dirs)
     | l ->
       anomaly ~label:locstr
-	(str ("ambiguous name "^s^" can represent ") ++
+	(str "ambiguous name " ++ str s ++ str " can represent " ++
 	   prlist_with_sep pr_comma
 	   (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
-	   str (" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	   str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
 	   prlist_with_sep pr_comma pr_dirpath dirs)
 
 let gen_constant_in_modules locstr dirs s =
@@ -86,7 +86,8 @@ let check_required_library d =
      (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
 *)
 (* or failing ...*)
-      error ("Library "^(DirPath.to_string dir)^" has to be required first.")
+      errorlabstrm "Coqlib.check_required_library"
+        (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects *)
-- 
cgit v1.2.3