Added a CString module.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7

20 files changed, 252 insertions, 130 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index bd3c5e00f2..e493cec03a 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -10,6 +10,7 @@ Unicode
 Errors
 CObj
 CList
+CString
 CArray
 Util
 Option
diff --git a/dev/printers.mllib b/dev/printers.mllib
index f0221a9c51..e6ecb8c56c 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -12,6 +12,7 @@ Unicode
 Errors
 CObj
 CList
+CString
 CArray
 Util
 Bigint
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index ee1bb32584..757df76a6a 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -8,6 +8,7 @@ Loc
 Compat
 Errors
 CList
+CString
 CArray
 Util
 Bigint
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b651053dba..6cfe74382d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -282,7 +282,7 @@ let drop_implicits_in_patt cst nb_expl args =
 let has_curly_brackets ntn =
   String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
     String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
-    string_string_contains ~where:ntn ~what:" { _ } ")
+    String.string_contains ~where:ntn ~what:" { _ } ")
 
 let rec wildcards ntn n =
   if n = String.length ntn then []
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a6b207c1da..cb95af7334 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -137,7 +137,7 @@ let explain_non_linear_pattern id =
   str "The variable " ++ pr_id id ++ str " is bound several times in pattern"
 
 let explain_bad_patterns_number n1 n2 =
-  str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++
+  str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++
   str " but found " ++ int n2
 
 let explain_internalization_error e =
diff --git a/interp/notation.ml b/interp/notation.ml
index d7f539f2f7..8483e18a99 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -641,7 +641,7 @@ let decompose_notation_key s =
     let tok =
       match String.sub s n (pos-n) with
       | "_" -> NonTerminal (id_of_string "_")
-      | s -> Terminal (drop_simple_quotes s) in
+      | s -> Terminal (String.drop_simple_quotes s) in
     decomp_ntn (tok::dirs) (pos+1)
   in
     decomp_ntn [] 0
diff --git a/lib/cString.ml b/lib/cString.ml
new file mode 100644
index 0000000000..6bc7c47295
--- /dev/null
+++ b/lib/cString.ml
@@ -0,0 +1,152 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** FIXME: use module type of *)
+module type S =
+sig
+  external length : string -> int = "%string_length"
+  external get : string -> int -> char = "%string_safe_get"
+  external set : string -> int -> char -> unit = "%string_safe_set"
+  external create : int -> string = "caml_create_string"
+  val make : int -> char -> string
+  val copy : string -> string
+  val sub : string -> int -> int -> string
+  val fill : string -> int -> int -> char -> unit
+  val blit : string -> int -> string -> int -> int -> unit
+  val concat : string -> string list -> string
+  val iter : (char -> unit) -> string -> unit
+  val escaped : string -> string
+  val index : string -> char -> int
+  val rindex : string -> char -> int
+  val index_from : string -> int -> char -> int
+  val rindex_from : string -> int -> char -> int
+  val contains : string -> char -> bool
+  val contains_from : string -> int -> char -> bool
+  val rcontains_from : string -> int -> char -> bool
+  val uppercase : string -> string
+  val lowercase : string -> string
+  val capitalize : string -> string
+  val uncapitalize : string -> string
+  type t = string
+  val compare: t -> t -> int
+  external unsafe_get : string -> int -> char = "%string_unsafe_get"
+  external unsafe_set : string -> int -> char -> unit = "%string_unsafe_set"
+  external unsafe_blit :
+    string -> int -> string -> int -> int -> unit = "caml_blit_string" "noalloc"
+  external unsafe_fill :
+    string -> int -> int -> char -> unit = "caml_fill_string" "noalloc"
+end
+
+module type ExtS =
+sig
+  include S
+  external equal : string -> string -> bool = "caml_string_equal"
+  val explode : string -> string list
+  val implode : string list -> string
+  val strip : string -> string
+  val map : (char -> char) -> string -> string
+  val drop_simple_quotes : string -> string
+  val string_index_from : string -> int -> string -> int
+  val string_contains : where:string -> what:string -> bool
+  val plural : int -> string -> string
+  val ordinal : int -> string
+  val split : char -> string -> string list
+end
+
+include String
+
+external equal : string -> string -> bool = "caml_string_equal"
+
+
+let explode s =
+  let rec explode_rec n =
+    if n >= String.length s then
+      []
+    else
+      String.make 1 (String.get s n) :: explode_rec (succ n)
+  in
+  explode_rec 0
+
+let implode sl = String.concat "" sl
+
+let is_blank = function
+  | ' ' | '\r' | '\t' | '\n' -> true
+  | _ -> false
+
+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 map f s =
+  let l = String.length s in
+  let r = String.create l in
+  for i = 0 to (l - 1) do r.[i] <- f (s.[i]) done;
+  r
+
+let drop_simple_quotes s =
+  let n = String.length s in
+  if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
+
+(* substring searching... *)
+
+(* gdzie = where, co = what *)
+(* gdzie=gdzie(string) gl=gdzie(length) gi=gdzie(index) *)
+let rec is_sub gdzie gl gi co cl ci =
+  (ci>=cl) ||
+  ((String.unsafe_get gdzie gi = String.unsafe_get co ci) &&
+   (is_sub gdzie gl (gi+1) co cl (ci+1)))
+
+let rec raw_str_index i gdzie l c co cl =
+  (* First adapt to ocaml 3.11 new semantics of index_from *)
+  if (i+cl > l) then raise Not_found;
+  (* Then proceed as in ocaml < 3.11 *)
+  let i' = String.index_from gdzie i c in
+    if (i'+cl <= l) && (is_sub gdzie l i' co cl 0) then i' else
+      raw_str_index (i'+1) gdzie l c co cl
+
+let string_index_from gdzie i co =
+  if co="" then i else
+    raw_str_index i gdzie (String.length gdzie)
+      (String.unsafe_get co 0) co (String.length co)
+
+let string_contains ~where ~what =
+  try
+    let _ = string_index_from where 0 what in true
+  with
+      Not_found -> false
+
+let plural n s = if n<>1 then s^"s" else s
+
+let ordinal n =
+  let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+  string_of_int n ^ s
+
+(* 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
diff --git a/lib/cString.mli b/lib/cString.mli
new file mode 100644
index 0000000000..d7ce35b009
--- /dev/null
+++ b/lib/cString.mli
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
+
+(** Module type [S] is the one from OCaml Stdlib. *)
+module type S =
+sig
+  external length : string -> int = "%string_length"
+  external get : string -> int -> char = "%string_safe_get"
+  external set : string -> int -> char -> unit = "%string_safe_set"
+  external create : int -> string = "caml_create_string"
+  val make : int -> char -> string
+  val copy : string -> string
+  val sub : string -> int -> int -> string
+  val fill : string -> int -> int -> char -> unit
+  val blit : string -> int -> string -> int -> int -> unit
+  val concat : string -> string list -> string
+  val iter : (char -> unit) -> string -> unit
+  val escaped : string -> string
+  val index : string -> char -> int
+  val rindex : string -> char -> int
+  val index_from : string -> int -> char -> int
+  val rindex_from : string -> int -> char -> int
+  val contains : string -> char -> bool
+  val contains_from : string -> int -> char -> bool
+  val rcontains_from : string -> int -> char -> bool
+  val uppercase : string -> string
+  val lowercase : string -> string
+  val capitalize : string -> string
+  val uncapitalize : string -> string
+  type t = string
+  val compare: t -> t -> int
+  external unsafe_get : string -> int -> char = "%string_unsafe_get"
+  external unsafe_set : string -> int -> char -> unit = "%string_unsafe_set"
+  external unsafe_blit :
+    string -> int -> string -> int -> int -> unit = "caml_blit_string" "noalloc"
+  external unsafe_fill :
+    string -> int -> int -> char -> unit = "caml_fill_string" "noalloc"
+end
+
+module type ExtS =
+sig
+  include S
+  external equal : string -> string -> bool = "caml_string_equal"
+  val explode : string -> string list
+  val implode : string list -> string
+  val strip : string -> string
+  val map : (char -> char) -> string -> string
+  val drop_simple_quotes : string -> string
+  val string_index_from : string -> int -> string -> int
+  val string_contains : where:string -> what:string -> bool
+  val plural : int -> string -> string
+  val ordinal : int -> string
+  val split : char -> string -> string list
+end
+
+include ExtS
diff --git a/lib/clib.mllib b/lib/clib.mllib
index f5fd721135..1f4707fda5 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -5,6 +5,7 @@ Coq_config
 Deque
 CObj
 CList
+CString
 CArray
 Util
 Serialize
diff --git a/lib/envars.ml b/lib/envars.ml
index 846391d838..27579e4eaa 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -102,7 +102,7 @@ let docdir () =
 
 let path_to_list p =
   let sep = if Sys.os_type = "Win32" then ';' else ':' in
-    Util.split_string_at sep p
+    Util.String.split sep p
 
 let xdg_data_home warning =
   coqify
@@ -170,7 +170,7 @@ let camllib () =
     let camlbin = camlbin () in
     let com = (Filename.concat camlbin "ocamlc") ^ " -where" in
     let _,res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in
-    Util.strip res
+    Util.String.strip res
 
 let camlp4bin () =
   if !Flags.camlp4bin_spec then !Flags.camlp4bin else
@@ -187,5 +187,5 @@ let camlp4lib () =
     let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in
     let ex,res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in
     match ex with
-      |Unix.WEXITED 0 -> Util.strip res
+      |Unix.WEXITED 0 -> Util.String.strip res
       |_ -> "/dev/null"
diff --git a/lib/util.ml b/lib/util.ml
index 84249e6aec..fcbd969ab5 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -36,92 +36,10 @@ let is_blank = function
 
 (* Strings *)
 
-let explode s =
-  let rec explode_rec n =
-    if n >= String.length s then
-      []
-    else
-      String.make 1 (String.get s n) :: explode_rec (succ n)
-  in
-  explode_rec 0
-
-let implode sl = String.concat "" sl
-
-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 string_map f s =
-  let l = String.length s in
-  let r = String.create l in
-  for i = 0 to (l - 1) do r.[i] <- f (s.[i]) done;
-  r
-
-let drop_simple_quotes s =
-  let n = String.length s in
-  if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
-
-(* substring searching... *)
-
-(* gdzie = where, co = what *)
-(* gdzie=gdzie(string) gl=gdzie(length) gi=gdzie(index) *)
-let rec is_sub gdzie gl gi co cl ci =
-  (ci>=cl) ||
-  ((String.unsafe_get gdzie gi = String.unsafe_get co ci) &&
-   (is_sub gdzie gl (gi+1) co cl (ci+1)))
-
-let rec raw_str_index i gdzie l c co cl =
-  (* First adapt to ocaml 3.11 new semantics of index_from *)
-  if (i+cl > l) then raise Not_found;
-  (* Then proceed as in ocaml < 3.11 *)
-  let i' = String.index_from gdzie i c in
-    if (i'+cl <= l) && (is_sub gdzie l i' co cl 0) then i' else
-      raw_str_index (i'+1) gdzie l c co cl
-
-let string_index_from gdzie i co =
-  if co="" then i else
-    raw_str_index i gdzie (String.length gdzie)
-      (String.unsafe_get co 0) co (String.length co)
-
-let string_string_contains ~where ~what =
-  try
-    let _ = string_index_from where 0 what in true
-  with
-      Not_found -> false
-
-let plural n s = if n<>1 then s^"s" else s
-
-let ordinal n =
-  let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
-  string_of_int n ^ s
-
-(* string parsing *)
-
-let split_string_at 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
+module String : CString.ExtS = CString
 
 let parse_loadpath s =
-  let l = split_string_at '/' s in
+  let l = String.split '/' s in
   if List.mem "" l then
     invalid_arg "parse_loadpath: find an empty dir in loadpath";
   l
@@ -137,14 +55,8 @@ let subst_command_placeholder s t =
   done;
   Buffer.contents buff
 
-module StringOrd =
-struct
-  type t = string
-  external compare : string -> string -> int = "caml_string_compare"
-end
-
-module Stringset = Set.Make(StringOrd)
-module Stringmap = Map.Make(StringOrd)
+module Stringset = Set.Make(String)
+module Stringmap = Map.Make(String)
 
 (* Lists *)
 
diff --git a/lib/util.mli b/lib/util.mli
index 694e79ce4a..6dc6c703dd 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -36,16 +36,7 @@ val is_blank : char -> bool
 
 (** {6 Strings. } *)
 
-val explode : string -> string list
-val implode : string list -> string
-val strip : string -> string
-val string_map : (char -> char) -> string -> string
-val drop_simple_quotes : string -> string
-val string_index_from : string -> int -> string -> int
-val string_string_contains : where:string -> what:string -> bool
-val plural : int -> string -> string
-val ordinal : int -> string
-val split_string_at : char -> string -> string list
+module String : CString.ExtS
 
 (** Substitute %s in the first chain by the second chain *)
 val subst_command_placeholder : string -> string -> string
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 4322ac95fa..dd3b65b908 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -413,7 +413,7 @@ let msg_non_implicit r n id =
     | Anonymous -> ""
     | Name id -> "(" ^ string_of_id id ^ ") "
   in
-  "The " ^ (ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r)
+  "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r)
 
 let error_non_implicit msg =
   err (str (msg ^ " still occurs after extraction.") ++
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 8369972284..333d3948dc 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -705,7 +705,7 @@ let replace_term = replace_term_gen eq_constr
 let error_invalid_occurrence l =
   let l = List.uniquize (List.sort Pervasives.compare l) in
   errorlabstrm ""
-    (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++
+    (str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ") ++
      prlist_with_sep spc int l ++ str ".")
 
 let pr_position (cl,pos) =
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 721d9b6c8a..41882acb4b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -734,7 +734,7 @@ let rec pr_vernac = function
 
  | VernacDeclareInstances (glob, ids) ->
      hov 1 (pr_non_locality (not glob) ++
-               str"Existing" ++ spc () ++ str(plural (List.length ids) "Instance") ++
+               str"Existing" ++ spc () ++ str(String.plural (List.length ids) "Instance") ++
                spc () ++ prlist_with_sep spc pr_reference ids)
 
  | VernacDeclareClass id ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 7fbbc0a2ec..3136847b03 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -85,7 +85,7 @@ let pr_impl_name imp = pr_id (name_of_implicit imp)
 let print_impargs_by_name max = function
   | []  -> []
   | impls ->
-     [hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++
+     [hov 0 (str (String.plural (List.length impls) "Argument") ++ spc() ++
       prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++
       str (conjugate_verb_to_be impls) ++ str" implicit" ++
       (if max then strbrk " and maximally inserted" else mt()))]
@@ -111,7 +111,7 @@ let print_impargs_list prefix l =
 	   (if n1 = n2 then int_or_no n2 else
 	    if n1 = 0 then str "less than " ++ int n2
 	    else int n1 ++ str " to " ++ int_or_no n2) ++
-	    str (plural n2 " argument") ++ str ":";
+	    str (String.plural n2 " argument") ++ str ":";
           v 0 (prlist_with_sep cut (fun x -> x)
 	    (if List.exists is_status_implicit imps
 	    then print_one_impargs_list imps
@@ -166,12 +166,12 @@ let print_simpl_behaviour ref =
      let pp_nomatch = spc() ++ if nomatch then
        str "avoiding to expose match constructs" else str"" in
      let pp_recargs = spc() ++ str "when the " ++
-       pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (plural (List.length recargs) " argument") ++
-       str (plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
+       pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (String.plural (List.length recargs) " argument") ++
+       str (String.plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
        str " to a constructor" in
      let pp_nargs =
        spc() ++ str "when applied to " ++ int nargs ++
-       str (plural nargs " argument") in
+       str (String.plural nargs " argument") in
      [hov 2 (str "The simpl tactic " ++
      match recargs, nargs, never with
      | _,_, true -> str "never unfolds " ++ pr_global ref
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 39c669f427..2a8722ea99 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1215,7 +1215,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
   begin match expctdnumopt with
     | Some n when n <> nconstr ->
 	error ("Not an inductive goal with "^
-	       string_of_int n^plural n " constructor"^".")
+	       string_of_int n ^ String.plural n " constructor"^".")
     | _ -> ()
   end;
   if i > nconstr then error "Not enough constructors."
@@ -1283,7 +1283,7 @@ let register_subst_one f =
 
 let error_unexpected_extra_pattern loc nb pat =
   let s1,s2,s3 = match pat with
-  | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no"
+  | IntroIdentifier _ -> "name", (String.plural nb " introduction pattern"), "no"
   | _ -> "introduction pattern", "", "none" in
   user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++
     (if Int.equal nb 0 then (str s3 ++ str s2) else
@@ -1883,7 +1883,7 @@ let expand_hyp id = tclTHEN (tclTRY (unfold_body id)) (clear [id])
 let check_unused_names names =
   if names <> [] & Flags.is_verbose () then
     msg_warning
-      (str"Unused introduction " ++ str (plural (List.length names) "pattern")
+      (str"Unused introduction " ++ str (String.plural (List.length names) "pattern")
        ++ str": " ++ prlist_with_sep spc pr_intro_pattern names)
 
 let rec consume_pattern avoid id isdep gl = function
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b6d1f981c7..ac86a04b95 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -169,7 +169,7 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
   let nargs = Array.length randl in
 (*  let pe = pr_ne_context_of (str "in environment") env in*)
   let pr,prt = pr_ljudge_env env rator in
-  let term_string1 = str (plural nargs "term") in
+  let term_string1 = str (String.plural nargs "term") in
   let term_string2 =
     if nargs>1 then str "The " ++ pr_nth n ++ str " term" else str "This term" in
   let appl = prvect_with_sep fnl
@@ -204,7 +204,7 @@ let explain_cant_apply_not_functional env sigma rator randl =
   (* pe ++ *) fnl () ++
   str "The expression" ++ brk(1,1) ++ pr ++ spc () ++
   str "of type" ++ brk(1,1) ++ prt ++ spc () ++
-  str "cannot be applied to the " ++ str (plural nargs "term") ++ fnl () ++
+  str "cannot be applied to the " ++ str (String.plural nargs "term") ++ fnl () ++
   str " " ++ v 0 appl
 
 let explain_unexpected_type env sigma actual_type expected_type =
@@ -448,7 +448,7 @@ let explain_cannot_unify_binding_type env m n =
 
 let explain_cannot_find_well_typed_abstraction env p l =
   str "Abstracting over the " ++
-  str (plural (List.length l) "term") ++ spc () ++
+  str (String.plural (List.length l) "term") ++ spc () ++
   hov 0 (pr_enum (pr_lconstr_env env) l) ++ spc () ++
   str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++
   str "which is ill-typed."
@@ -757,7 +757,7 @@ let explain_refiner_bad_type arg ty conclty =
 
 let explain_refiner_unresolved_bindings l =
   str "Unable to find an instance for the " ++
-  str (plural (List.length l) "variable") ++ spc () ++
+  str (String.plural (List.length l) "variable") ++ spc () ++
   prlist_with_sep pr_comma pr_name l ++ str"."
 
 let explain_refiner_cannot_apply t harg =
@@ -817,12 +817,12 @@ let error_ill_formed_constructor env id c v nparams nargs =
   (* warning: because of implicit arguments it is difficult to say which
      parameters must be explicitly given *)
   (if nparams<>0 then
-    strbrk " applied to its " ++ str (plural nparams "parameter")
+    strbrk " applied to its " ++ str (String.plural nparams "parameter")
   else
     mt()) ++
   (if nargs<>0 then
      str (if nparams<>0 then " and" else " applied") ++
-     strbrk " to some " ++ str (plural nargs "argument")
+     strbrk " to some " ++ str (String.plural nargs "argument")
    else
      mt()) ++ str "."
 
@@ -955,7 +955,7 @@ let explain_unused_clause env pats =
 
 let explain_non_exhaustive env pats =
   str "Non exhaustive pattern-matching: no clause found for " ++
-  str (plural (List.length pats) "pattern") ++
+  str (String.plural (List.length pats) "pattern") ++
   spc () ++ hov 0 (pr_sequence pr_cases_pattern pats)
 
 let explain_cannot_infer_predicate env typs =
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 3451471573..1a61982eac 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -359,7 +359,7 @@ let rec raw_analyze_notation_tokens = function
   | String x :: sl when Lexer.is_ident x ->
       NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl
   | String s :: sl ->
-      Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl
+      Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl
   | WhiteSpace n :: sl ->
       Break n :: raw_analyze_notation_tokens sl
 
@@ -571,7 +571,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
       when s' = String.make (String.length s') ' ' ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
   | Terminal s :: symbs, (UnpTerminal s') :: fmt
-      when s = drop_simple_quotes s' ->
+      when s = String.drop_simple_quotes s' ->
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
   | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' ->
       let i = List.index s vars in
diff --git a/toplevel/search.ml b/toplevel/search.ml
index d66260c608..23e4596b0d 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -212,7 +212,7 @@ let filter_by_module_from_list = function
 let filter_blacklist gr _ _ =
   let name = full_name_of_reference gr in
   let l = SearchBlacklist.elements () in
-  List.for_all (fun str -> not (string_string_contains ~where:name ~what:str)) l
+  List.for_all (fun str -> not (String.string_contains ~where:name ~what:str)) l
 
 let (&&&&&) f g x y z = f x y z && g x y z
 
@@ -237,7 +237,7 @@ type glob_search_about_item =
 
 let search_about_item (itemref,typ) = function
   | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ
-  | GlobSearchString s -> string_string_contains ~where:(name_of_reference itemref) ~what:s
+  | GlobSearchString s -> String.string_contains ~where:(name_of_reference itemref) ~what:s
 
 let raw_search_about filter_modules display_function l =
   let filter ref' env typ =