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.
---
 pretyping/unification.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 01e1154e58..c2281e13a5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1528,7 +1528,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context x (named_context env) then
-      error ("The variable "^(Id.to_string x)^" is already declared.")
+      errorlabstrm "Unification.make_abstraction_core"
+        (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
       x
   in
-- 
cgit v1.2.3