Extract Rocq strings to OCaml strings instead of OCaml lists of characters

Native string extraction is now supported by all the Coq versions we support.

Author: xavierleroy

extraction/extraction.v

@@ -25,7 +25,7 @@ Require Parser.
 Require Initializers.
 
 (* Standard lib *)
-From Coq Require Import ExtrOcamlBasic ExtrOcamlString.
+From Coq Require Import ExtrOcamlBasic ExtrOcamlNativeString.
 
 (* Coqlib *)
 Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".

lib/Camlcoq.ml

@@ -376,27 +376,11 @@ let first_unused_ident () =
 
 (* Strings *)
 
-let camlstring_of_coqstring (s: char list) =
-  let r = Bytes.create (List.length s) in
-  let rec fill pos = function
-  | [] -> r
-  | c :: s -> Bytes.set r pos c; fill (pos + 1) s
-  in Bytes.to_string (fill 0 s)
-
-let coqstring_of_camlstring s =
-  let rec cstring accu pos =
-    if pos < 0 then accu else cstring (s.[pos] :: accu) (pos - 1)
-  in cstring [] (String.length s - 1)
-
-let coqstring_uppercase_ascii_of_camlstring s =
-  let rec cstring accu pos =
-    if pos < 0 then accu else
-    let d = if s.[pos] >= 'a' && s.[pos] <= 'z' then
-      Char.chr (Char.code s.[pos] - 32)
-    else
-      s.[pos] in
-    cstring (d :: accu) (pos - 1)
-  in cstring [] (String.length s - 1)
+let camlstring_of_coqstring s = s
+
+let coqstring_of_camlstring s = s
+
+let coqstring_uppercase_ascii_of_camlstring s = String.uppercase_ascii s
 
 (* Floats *)