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/syntax_def.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/syntax_def.ml')

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 9be7abcfe0..d2709d5e3c 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -99,7 +99,7 @@ let verbose_compat kn def = function
       | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
       | _ -> str " is a compatibility notation"
     in
-    let since = str (" since Coq > " ^ Flags.pr_version v ^ ".") in
+    let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
     act (pr_syndef kn ++ pp_def ++ since)
   | _ -> ()
 
-- 
cgit v1.2.3