From 69c4e7cfa0271f024b2178082e4be2e3ca3be263 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 5 Feb 2017 01:46:41 +0100 Subject: Extraction: avoid deprecated functions of module String - A few tweaks of string are now done via the Bytes module - lots of String.capitalize_ascii and co --- plugins/extraction/common.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'plugins/extraction/common.ml') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index de97ba97c..b93a76b96 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -92,9 +92,11 @@ let begins_with_CoqXX s = let unquote s = if lang () != Scheme then s else - let s = String.copy s in - for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done; - s + let b = Bytes.of_string s in + for i=0 to Bytes.length b - 1 do + if Bytes.get b i == '\'' then Bytes.set b i '~' + done; + Bytes.to_string b let rec qualify delim = function | [] -> assert false @@ -110,12 +112,13 @@ let pseudo_qualify = qualify "__" let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false -let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id)) +let lowercase_id id = + Id.of_string (String.uncapitalize_ascii (ascii_of_id id)) let uppercase_id id = let s = ascii_of_id id in assert (not (String.is_empty s)); if s.[0] == '_' then Id.of_string ("Coq_"^s) - else Id.of_string (String.capitalize s) + else Id.of_string (String.capitalize_ascii s) type kind = Term | Type | Cons | Mod -- cgit v1.2.3