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

4 files changed, 13 insertions, 13 deletions

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