[clib] Deprecate string functions available in OCaml 4.05

- `CString.strip -> String.trim`
- `CString.split -> String.split_on_char`

As noted by @ppedrot there are some small differences on semantics:

> OCaml's `trim` also takes line feeds (LF) into account. Similarly,
> OCaml's `split` never returns an empty list whereas Coq's `split`
> does on the empty string.

8 files changed, 17 insertions, 40 deletions

diff --git a/clib/cString.ml b/clib/cString.ml
index b178cbbd2c..111be3da82 100644
--- a/clib/cString.ml
+++ b/clib/cString.ml
@@ -18,6 +18,7 @@ sig
   val explode : string -> string list
   val implode : string list -> string
   val strip : string -> string
+  [@@ocaml.deprecated "Use [trim]"]
   val drop_simple_quotes : string -> string
   val string_index_from : string -> int -> string -> int
   val string_contains : where:string -> what:string -> bool
@@ -25,6 +26,7 @@ sig
   val conjugate_verb_to_be : int -> string
   val ordinal : int -> string
   val split : char -> string -> string list
+  [@@ocaml.deprecated "Use [split_on_char]"]
   val is_sub : string -> string -> int -> bool
   module Set : Set.S with type elt = t
   module Map : CMap.ExtS with type key = t and module Set := Set
@@ -55,26 +57,9 @@ let explode s =
 
 let implode sl = String.concat "" sl
 
-let is_blank = function
-  | ' ' | '\r' | '\t' | '\n' -> true
-  | _ -> false
-
 let is_empty s = String.length s = 0
 
-let strip s =
-  let n = String.length s in
-  let rec lstrip_rec i =
-    if i < n && is_blank s.[i] then
-      lstrip_rec (i+1)
-    else i
-  in
-  let rec rstrip_rec i =
-    if i >= 0 && is_blank s.[i] then
-      rstrip_rec (i-1)
-    else i
-  in
-  let a = lstrip_rec 0 and b = rstrip_rec (n-1) in
-  String.sub s a (b-a+1)
+let strip = String.trim
 
 let drop_simple_quotes s =
   let n = String.length s in
@@ -139,17 +124,7 @@ let ordinal n =
 
 (* string parsing *)
 
-let split c s =
-  let len = String.length s in
-  let rec split n =
-    try
-      let pos = String.index_from s n c in
-      let dir = String.sub s n (pos-n) in
-      dir :: split (succ pos)
-    with
-      | Not_found -> [String.sub s n (len-n)]
-  in
-  if Int.equal len 0 then [] else split 0
+let split = String.split_on_char
 
 module Self =
 struct
diff --git a/clib/cString.mli b/clib/cString.mli
index df25a3821a..a73c2729d0 100644
--- a/clib/cString.mli
+++ b/clib/cString.mli
@@ -31,7 +31,8 @@ sig
   (** [implode [s1; ...; sn]] returns [s1 ^ ... ^ sn] *)
 
   val strip : string -> string
-  (** Remove the surrounding blank characters from a string *)
+  (** Alias for [String.trim] *)
+  [@@ocaml.deprecated "Use [trim]"]
 
   val drop_simple_quotes : string -> string
   (** Remove the eventual first surrounding simple quotes of a string. *)
@@ -52,7 +53,8 @@ sig
   (** Generate the ordinal number in English. *)
 
   val split : char -> string -> string list
-  (** [split c s] splits [s] into sequences separated by [c], excluded. *)
+  (** [split c s] alias of [String.split_on_char] *)
+  [@@ocaml.deprecated "Use [split_on_char]"]
 
   val is_sub : string -> string -> int -> bool
   (** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 00d43e6e64..4190f43680 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -769,7 +769,7 @@ let coqtop_arguments sn =
   let box = dialog#action_area in
   let ok = GButton.button ~stock:`OK ~packing:box#add () in
   let ok_cb () =
-    let nargs = CString.split ' ' entry#text in
+    let nargs = String.split_on_char ' ' entry#text in
     if nargs <> args then
       let failed = Coq.filter_coq_opts nargs in
       match failed with
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 9f04ced1c3..6dc922c225 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -167,7 +167,7 @@ object
   method into l =
     try
       Some (CList.map (fun s ->
-        let split = CString.split sep s in
+        let split = String.split_on_char sep s in
         CList.nth split 0, CList.nth split 1) l)
     with Failure _ -> None
 end
diff --git a/lib/envars.ml b/lib/envars.ml
index cf76b6ebc8..724a3dddc7 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -34,7 +34,7 @@ let home ~warn =
 
 let path_to_list p =
   let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in
-    String.split sep p
+    String.split_on_char sep p
 
 let expand_path_macros ~warn s =
   let rec expand_atom s i =
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index d22bd4967a..db7dcfa6ef 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -260,7 +260,7 @@ let string_of_call ck =
     ) in
   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
+  String.trim s
 
 let rec merge_sub_tree name tree acc =
   try
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 0e56cc3c0f..d91c4f0b34 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -248,7 +248,7 @@ let rec logic_gcd acc = function
 
 let generate_conf_doc oc { defs; q_includes; r_includes } =
   let includes = List.map (forget_source > snd) (q_includes @ r_includes) in
-  let logpaths = List.map (CString.split '.') includes in
+  let logpaths = List.map (String.split_on_char '.') includes in
   let gcd = logic_gcd [] logpaths in
   let root =
     if gcd = [] then
@@ -378,8 +378,8 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
   | _ -> assert false
 
 let share_prefix s1 s2 =
-  let s1 = CString.split '.' s1 in
-  let s2 = CString.split '.' s2 in
+  let s1 = String.split_on_char '.' s1 in
+  let s2 = String.split_on_char '.' s2 in
   match s1, s2 with
   | x :: _ , y :: _ -> x = y
   | _ -> false
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 06d9ba3436..9918adfed3 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -244,7 +244,7 @@ let get_float opt n =
     prerr_endline ("Error: float expected after option "^opt); exit 1
 
 let get_host_port opt s =
-  match CString.split ':' s with
+  match String.split_on_char ':' s with
   | [host; portr; portw] ->
        Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
   | ["stdfds"] -> Some Spawned.AnonPipe
@@ -255,7 +255,7 @@ let get_host_port opt s =
 let get_error_resilience opt = function
   | "on" | "all" | "yes" -> `All
   | "off" | "no" -> `None
-  | s -> `Only (CString.split ',' s)
+  | s -> `Only (String.split_on_char ',' s)
 
 let get_priority opt s =
   try CoqworkmgrApi.priority_of_string s