From fa895511eaa1c374c72ea2096c1dfb33dfbee379 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 13:36:52 +0100
Subject: [safe-string] ltac/profile_ltac

No functional change, one extra copy introduced but it seems hard to
avoid.
---
 plugins/ltac/profile_ltac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 2514ededb0..58123f63ef 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -257,7 +257,7 @@ let string_of_call ck =
          (Pptactic.pr_glob_tactic (Global.env ())
             te)
     ) in
-  for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done;
+  let s = String.map (fun c -> if c = '\n' then ' ' else c) s in
   let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in
   CString.strip s
 
-- 
cgit v1.2.3