From 3a050f305293676ccf66d415ab386d9521f0f765 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 04:04:33 +0100
Subject: [safe_string] kernel/term_typing

No functional change, we create the new string beforehand and
`id_of_string` will become a noop with `-safe-string`.
---
 kernel/term_typing.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3a0d1a2a5e..b9cf8101da 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -76,8 +76,7 @@ let inline_side_effects env body ctx side_eff =
     let cbl = List.filter not_exists cbl in
     let cname c = 
       let name = string_of_con c in
-      for i = 0 to String.length name - 1 do
-        if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done;
+      let name = String.map (fun c -> if c == '.' || c == '#' then '_' else c) name in
       Name (id_of_string name) in
     let rec sub c i x = match kind_of_term x with
       | Const (c', _) when eq_constant c c' -> mkRel i
-- 
cgit v1.2.3