Added a CString module.

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

3 files changed, 11 insertions, 11 deletions

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 =