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

1 files changed, 8 insertions, 5 deletions

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