Moved Stringset and Stringmap to String namespace.

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

17 files changed, 77 insertions, 63 deletions

diff --git a/ide/preferences.ml b/ide/preferences.ml
index ed4f4cd1f..3116be1af 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -236,9 +236,9 @@ let save_pref () =
   let () = try GtkData.AccelMap.save accel_file with _ -> () in
   let p = current in
 
-    let add = Util.Stringmap.add in
+    let add = Util.String.Map.add in
     let (++) x f = f x in
-    Util.Stringmap.empty ++
+    Util.String.Map.empty ++
     add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++
     add "cmd_coqc" [p.cmd_coqc] ++
     add "cmd_make" [p.cmd_make] ++
@@ -302,7 +302,7 @@ let load_pref () =
 
     let m = Config_lexer.load_file loaded_pref_file in
     let np = current in
-    let set k f = try let v = Util.Stringmap.find k m in f v with _ -> () in
+    let set k f = try let v = Util.String.Map.find k m in f v with _ -> () in
     let set_hd k f = set k (fun v -> f (List.hd v)) in
     let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in
     let set_int k f = set_hd k (fun v -> f (int_of_string v)) in
diff --git a/lib/cString.ml b/lib/cString.ml
index fd375c5c3..b34b21957 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -58,6 +58,8 @@ sig
   val ordinal : int -> string
   val split : char -> string -> string list
   val is_sub : string -> string -> int -> bool
+  module Set : Set.S with type elt = t
+  module Map : Map.S with type key = t
 end
 
 include String
@@ -167,3 +169,12 @@ let split c s =
       | Not_found -> [String.sub s n (len-n)]
   in
   if Int.equal len 0 then [] else split 0
+
+module Self =
+struct
+  type t = string
+  let compare = compare
+end
+
+module Set = Set.Make(Self)
+module Map = Map.Make(Self)
diff --git a/lib/cString.mli b/lib/cString.mli
index 9f4a47f19..18679d310 100644
--- a/lib/cString.mli
+++ b/lib/cString.mli
@@ -87,6 +87,13 @@ sig
 
   val is_sub : string -> string -> int -> bool
   (** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *)
+
+  module Set : Set.S with type elt = t
+  (** Finite sets on [string] *)
+
+  module Map : Map.S with type key = t
+  (** Finite maps on [string] *)
+
 end
 
 include ExtS
diff --git a/lib/envars.ml b/lib/envars.ml
index a4629e50d..097ffe08e 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
+
 (** {1 Helper functions} *)
 
 let getenv_else s dft = try Sys.getenv s with Not_found -> dft ()
@@ -31,7 +33,7 @@ let home ~warn =
 
 let path_to_list p =
   let sep = if Sys.os_type = "Win32" then ';' else ':' in
-    Util.String.split sep p
+    String.split sep p
 
 let user_path () = 
   let path = try Sys.getenv "PATH" with _ -> raise Not_found in
@@ -161,7 +163,7 @@ let camllib () =
   else
     let com = ocamlc () ^ " -where" in
     let _, res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in
-    Util.String.strip res
+    String.strip res
 
 (** {2 Camlp4 paths} *)
 
@@ -187,7 +189,7 @@ let camlp4lib () =
     let com = camlp4 () ^ " -where" in
     let ex, res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in
     match ex with
-      | Unix.WEXITED 0 -> Util.String.strip res
+      | Unix.WEXITED 0 -> String.strip res
       | _ -> "/dev/null"
 
 (** {1 XDG utilities} *)
diff --git a/lib/util.ml b/lib/util.ml
index 91497f370..c2d290714 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -55,9 +55,6 @@ let subst_command_placeholder s t =
   done;
   Buffer.contents buff
 
-module Stringset = Set.Make(String)
-module Stringmap = Map.Make(String)
-
 (* Lists *)
 
 module List : CList.ExtS = CList
diff --git a/lib/util.mli b/lib/util.mli
index e6cb7fe9d..33812c200 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -42,9 +42,6 @@ module String : CString.ExtS
 val subst_command_placeholder : string -> string -> string
 val parse_loadpath : string -> string list
 
-module Stringset : Set.S with type elt = string
-module Stringmap : Map.S with type key = string
-
 (** {6 Lists. } *)
 
 module List : CList.ExtS
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 4adf9d02d..b8dd671cf 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -27,19 +27,19 @@ type 'a module_signature =
 
 type scope_subst = (string * string) list
 
-let scope_subst = ref (Stringmap.empty : string Stringmap.t)
+let scope_subst = ref (String.Map.empty : string String.Map.t)
 
 let add_scope_subst sc sc' =
-  scope_subst := Stringmap.add sc sc' !scope_subst
+  scope_subst := String.Map.add sc sc' !scope_subst
 
 let register_scope_subst scl =
   List.iter (fun (sc1,sc2) -> add_scope_subst sc1 sc2) scl
 
 let subst_scope sc =
- try Stringmap.find sc !scope_subst with Not_found -> sc
+ try String.Map.find sc !scope_subst with Not_found -> sc
 
 let reset_scope_subst () =
-  scope_subst := Stringmap.empty
+  scope_subst := String.Map.empty
 
 (** Which inline annotations should we honor, either None or the ones
     whose level is less or equal to the given integer *)
diff --git a/library/summary.ml b/library/summary.ml
index af5af37f1..a31f61c31 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -36,12 +36,12 @@ let internal_declare_summary sumname sdecl =
 let declare_summary sumname decl =
   internal_declare_summary (sumname^"-SUMMARY") decl
 
-type frozen = Dyn.t Stringmap.t
+type frozen = Dyn.t String.Map.t
 
 let freeze_summaries () =
-  let m = ref Stringmap.empty in
+  let m = ref String.Map.empty in
   Hashtbl.iter
-    (fun id decl -> m := Stringmap.add id (decl.freeze_function()) !m)
+    (fun id decl -> m := String.Map.add id (decl.freeze_function()) !m)
     summaries;
   !m
 
@@ -49,7 +49,7 @@ let freeze_summaries () =
 let unfreeze_summaries fs =
   Hashtbl.iter
     (fun id decl ->
-       try decl.unfreeze_function (Stringmap.find id fs)
+       try decl.unfreeze_function (String.Map.find id fs)
        with Not_found -> decl.init_function())
     summaries
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index fad762e9b..717b19e2c 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -73,10 +73,10 @@ and mk_clos_app_but f_map subs f args n =
 let interp_map l t =
   try Some(List.assoc_f eq_constr t l) with Not_found -> None
 
-let protect_maps = ref Stringmap.empty
-let add_map s m = protect_maps := Stringmap.add s m !protect_maps
+let protect_maps = ref String.Map.empty
+let add_map s m = protect_maps := String.Map.add s m !protect_maps
 let lookup_map map =
-  try Stringmap.find map !protect_maps
+  try String.Map.find map !protect_maps
   with Not_found ->
     errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 26e9f9eb5..5c65f55b5 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -60,7 +60,7 @@ type 'a extra_genarg_printer =
     (tolerability -> glob_tactic_expr -> std_ppcmds) ->
     'a -> std_ppcmds
 
-let genarg_pprule = ref Stringmap.empty
+let genarg_pprule = ref String.Map.empty
 
 let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) =
   let s = match unquote wit with
@@ -71,7 +71,7 @@ let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) =
   let f prc prlc prtac x = f prc prlc prtac (out_gen rawwit x) in
   let g prc prlc prtac x = g prc prlc prtac (out_gen globwit x) in
   let h prc prlc prtac x = h prc prlc prtac (out_gen wit x) in
-  genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule
+  genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule
 
 let pr_arg pr x = spc () ++ pr x
 
@@ -178,7 +178,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
             [a;b])
 	  x)
   | ExtraArgType s ->
-      try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
+      try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x
       with Not_found -> str "[no printer for " ++ str s ++ str "]"
 
 
@@ -223,7 +223,7 @@ let rec pr_glob_generic prc prlc prtac prpat x =
 	  (fun a b -> pr_sequence (pr_glob_generic prc prlc prtac prpat) [a;b])
 	  x)
   | ExtraArgType s ->
-      try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
+      try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
       with Not_found -> str "[no printer for " ++ str s ++ str "]"
 
 let rec pr_generic prc prlc prtac prpat x =
@@ -263,7 +263,7 @@ let rec pr_generic prc prlc prtac prpat x =
           [a;b])
 	  x)
   | ExtraArgType s ->
-      try pi3 (Stringmap.find s !genarg_pprule) prc prlc prtac x
+      try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x
       with Not_found -> str "[no printer for " ++ str s ++ str "]"
 
 let rec tacarg_using_rule_token pr_gen = function
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index aa3d13f8a..e4b8697d1 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -141,29 +141,29 @@ let is_reference = function PRef _ | PVar _ -> true | _ -> false
 
 (* table of custom reductino fonctions, not synchronized,
    filled via ML calls to [declare_reduction] *)
-let reduction_tab = ref Stringmap.empty
+let reduction_tab = ref String.Map.empty
 
 (* table of custom reduction expressions, synchronized,
    filled by command Declare Reduction *)
-let red_expr_tab = ref Stringmap.empty
+let red_expr_tab = ref String.Map.empty
 
 let declare_reduction s f =
-  if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab
+  if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
   then error ("There is already a reduction expression of name "^s)
-  else reduction_tab := Stringmap.add s f !reduction_tab
+  else reduction_tab := String.Map.add s f !reduction_tab
 
 let check_custom = function
   | ExtraRedExpr s ->
-      if not (Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab)
+      if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
       then error ("Reference to undefined reduction expression "^s)
   |_ -> ()
 
 let decl_red_expr s e =
-  if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab
+  if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
   then error ("There is already a reduction expression of name "^s)
   else begin
     check_custom e;
-    red_expr_tab := Stringmap.add s e !red_expr_tab
+    red_expr_tab := String.Map.add s e !red_expr_tab
   end
 
 let out_arg = function
@@ -188,9 +188,9 @@ let rec reduction_of_red_expr = function
   | Fold cl -> (fold_commands cl,DEFAULTcast)
   | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
   | ExtraRedExpr s ->
-      (try (Stringmap.find s !reduction_tab,DEFAULTcast)
+      (try (String.Map.find s !reduction_tab,DEFAULTcast)
       with Not_found ->
-	(try reduction_of_red_expr (Stringmap.find s !red_expr_tab)
+	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
 	 with Not_found ->
 	   error("unknown user-defined reduction \""^s^"\"")))
   | CbvVm (Some lp) ->
@@ -242,4 +242,4 @@ let declare_red_expr locality s expr =
 let _ = declare_summary "Declare Reduction"
   { freeze_function = (fun () -> !red_expr_tab);
     unfreeze_function = ((:=) red_expr_tab);
-    init_function = (fun () -> red_expr_tab := Stringmap.empty) }
+    init_function = (fun () -> red_expr_tab := String.Map.empty) }
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index bad5a6aa0..672b5bc45 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -58,10 +58,10 @@ module HintDN = Term_dnet.Make(HintIdent)(HintOpt)
 
 (* Summary and Object declaration *)
 let rewtab =
-  ref (Stringmap.empty : HintDN.t Stringmap.t)
+  ref (String.Map.empty : HintDN.t String.Map.t)
 
 let _ =
-  let init () = rewtab := Stringmap.empty in
+  let init () = rewtab := String.Map.empty in
   let freeze () = !rewtab in
   let unfreeze fs = rewtab := fs in
   Summary.declare_summary "autorewrite"
@@ -70,7 +70,7 @@ let _ =
       Summary.init_function     = init }
 
 let find_base bas =
- try Stringmap.find bas !rewtab
+ try String.Map.find bas !rewtab
  with
   Not_found ->
    errorlabstrm "AutoRewrite"
@@ -207,7 +207,7 @@ let cache_hintrewrite (_,(rbase,lrl)) =
   let base = try find_base rbase with _ -> HintDN.empty in
   let max = try fst (Util.List.last (HintDN.find_all base)) with _ -> 0 in
   let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
-    rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab
+    rewtab:=String.Map.add rbase (HintDN.union lrl base) !rewtab
 
 
 let subst_hintrewrite (subst,(rbase,list as node)) =
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 8dcb05615..9a8774b11 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -71,13 +71,13 @@ type intern_genarg_type =
     glob_sign -> raw_generic_argument -> glob_generic_argument
 
 let genarginterns =
-  ref (Stringmap.empty : intern_genarg_type Stringmap.t)
+  ref (String.Map.empty : intern_genarg_type String.Map.t)
 
 let add_intern_genarg id f =
-  genarginterns := Stringmap.add id f !genarginterns
+  genarginterns := String.Map.add id f !genarginterns
 
 let lookup_intern_genarg id =
-  try Stringmap.find id !genarginterns
+  try String.Map.find id !genarginterns
   with Not_found ->
     let msg = "No globalization function found for entry "^id in
     Pp.msg_warning (Pp.strbrk msg);
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0cfb4bb97..3f7cbb625 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -137,11 +137,11 @@ type interp_genarg_type =
     Evd.evar_map * typed_generic_argument
 
 let extragenargtab =
-  ref (Stringmap.empty : interp_genarg_type Stringmap.t)
+  ref (String.Map.empty : interp_genarg_type String.Map.t)
 let add_interp_genarg id f =
-  extragenargtab := Stringmap.add id f !extragenargtab
+  extragenargtab := String.Map.add id f !extragenargtab
 let lookup_interp_genarg id =
-  try Stringmap.find id !extragenargtab
+  try String.Map.find id !extragenargtab
   with Not_found ->
     let msg = "No interpretation function found for entry " ^ id in
     msg_warning (strbrk msg);
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index d5b4e3197..bbf4089ed 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -26,11 +26,11 @@ open Pretyping
 type subst_genarg_type =
     substitution -> glob_generic_argument -> glob_generic_argument
 let genargsubs =
-  ref (Stringmap.empty : subst_genarg_type Stringmap.t)
+  ref (String.Map.empty : subst_genarg_type String.Map.t)
 let add_genarg_subst id f =
-  genargsubs := Stringmap.add id f !genargsubs
+  genargsubs := String.Map.add id f !genargsubs
 let lookup_genarg_subst id =
-  try Stringmap.find id !genargsubs
+  try String.Map.find id !genargsubs
   with Not_found ->
     Pp.msg_warning (Pp.strbrk ("No substitution found for entry "^id));
     let dflt = fun _ x -> x in
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 9cbf5c1ce..722a1a748 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -35,8 +35,8 @@ type 'a scheme_kind = string
 let scheme_map = ref Indmap.empty
 
 let cache_one_scheme kind (ind,const) =
-  let map = try Indmap.find ind !scheme_map with Not_found -> Stringmap.empty in
-  scheme_map := Indmap.add ind (Stringmap.add kind const map) !scheme_map
+  let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in
+  scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map
 
 let cache_scheme (_,(kind,l)) =
   Array.iter (cache_one_scheme kind) l
@@ -168,7 +168,7 @@ let define_mutual_scheme kind internal names mind =
       define_mutual_scheme_base kind s f internal names mind
 
 let find_scheme kind (mind,i as ind) =
-  try Stringmap.find kind (Indmap.find ind !scheme_map)
+  try String.Map.find kind (Indmap.find ind !scheme_map)
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
   | s,IndividualSchemeFunction f ->
@@ -177,6 +177,6 @@ let find_scheme kind (mind,i as ind) =
       (define_mutual_scheme_base kind s f KernelSilent [] mind).(i)
 
 let check_scheme kind ind =
-  try let _ = Stringmap.find kind (Indmap.find ind !scheme_map) in true
+  try let _ = String.Map.find kind (Indmap.find ind !scheme_map) in true
   with Not_found -> false
 
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 7f55e8971..947b02924 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -237,31 +237,31 @@ let file_of_name name =
  * (linked or loaded with load_object). It is used not to load a
  * module twice. It is NOT the list of ML modules Coq knows. *)
 
-let known_loaded_modules = ref Stringset.empty
+let known_loaded_modules = ref String.Set.empty
 
 let add_known_module mname =
   let mname = String.capitalize mname in
-  known_loaded_modules := Stringset.add mname !known_loaded_modules
+  known_loaded_modules := String.Set.add mname !known_loaded_modules
 
 let module_is_known mname =
-  Stringset.mem (String.capitalize mname) !known_loaded_modules
+  String.Set.mem (String.capitalize mname) !known_loaded_modules
 
 (** A plugin is just an ML module with an initialization function. *)
 
-let known_loaded_plugins = ref Stringmap.empty
+let known_loaded_plugins = ref String.Map.empty
 
 let add_known_plugin init name =
   let name = String.capitalize name in
   add_known_module name;
-  known_loaded_plugins := Stringmap.add name init !known_loaded_plugins
+  known_loaded_plugins := String.Map.add name init !known_loaded_plugins
 
 let init_known_plugins () =
-  Stringmap.iter (fun _ f -> f()) !known_loaded_plugins
+  String.Map.iter (fun _ f -> f()) !known_loaded_plugins
 
 (** ml object = ml module or plugin *)
 
 let init_ml_object mname =
-  try Stringmap.find mname !known_loaded_plugins ()
+  try String.Map.find mname !known_loaded_plugins ()
   with Not_found -> ()
 
 let load_ml_object mname fname=
@@ -271,7 +271,7 @@ let load_ml_object mname fname=
 
 (* Summary of declared ML Modules *)
 
-(* List and not Stringset because order is important: most recent first. *)
+(* List and not String.Set because order is important: most recent first. *)
 
 let loaded_modules = ref []
 let get_loaded_modules () = List.rev !loaded_modules