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.
---
 proofs/redexpr.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 1383d75567..d25f7e9150 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
-- 
cgit v1.2.3