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/tactic_debug.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'proofs/tactic_debug.ml')

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 3cc81daf58..d7f4b5ead5 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -11,6 +11,7 @@ open Names
 open Pp
 open Tacexpr
 open Termops
+open Nameops
 
 let (prtac, tactic_printer) = Hook.make ()
 let (prmatchpatt, match_pattern_printer) = Hook.make ()
@@ -231,17 +232,16 @@ let db_pattern_rule debug num r =
 
 (* Prints the hypothesis pattern identifier if it exists *)
 let hyp_bound = function
-  | Anonymous -> " (unbound)"
-  | Name id -> " (bound to "^(Names.Id.to_string id)^")"
+  | Anonymous -> str " (unbound)"
+  | Name id -> str " (bound to " ++ pr_id id ++ str ")"
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,_,c) ido =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str "Hypothesis " ++
-           str ((Names.Id.to_string id)^(hyp_bound ido)^
-                " has been matched: ") ++ print_constr_env env c)
+    msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++
+                str " has been matched: " ++ print_constr_env env c)
   else return ()
 
 (* Prints the matched conclusion *)
@@ -266,8 +266,8 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^
-                " cannot match: ") ++
+    msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++
+                str " cannot match: " ++
            Hook.get prmatchpatt env sigma hyp)
   else return ()
 
-- 
cgit v1.2.3