ident au lieu de string pour le nom de base de qualid

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

5 files changed, 27 insertions, 25 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 57e58256e..853a22d12 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -420,7 +420,7 @@ let dirpath_of_global = function
 
 let is_global id =
   try 
-    let osp = Nametab.locate (make_qualid [] (string_of_id id)) in
+    let osp = Nametab.locate (make_qualid [] id) in
     list_prefix_of (dirpath_of_global osp) (Lib.cwd())
   with Not_found -> 
     false
diff --git a/library/global.ml b/library/global.ml
index c07452988..cdc7fdb18 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -63,9 +63,9 @@ let sp_of_global id = Environ.sp_of_global (env_of_safe_env !global_env) id
 
 let qualid_of_global ref =  
   let sp = sp_of_global ref in
-  let s = string_of_id (basename sp) in
+  let id = basename sp in
   let rec find_visible dir qdir =
-    let qid = make_qualid qdir s in
+    let qid = make_qualid qdir id in
     if (try Nametab.locate qid = ref with Not_found -> false) then qid
     else match dir with
       | [] -> qualid_of_sp sp
diff --git a/library/library.ml b/library/library.ml
index b0c1a2ecd..0ec028963 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -117,7 +117,7 @@ let rec open_module force s =
   if force or not m.module_opened then begin
     List.iter (fun (m,_,exp) -> if exp then open_module force m) m.module_deps;
     open_objects m.module_declarations;
-    Nametab.open_module_contents (make_qualid [] s); 
+    Nametab.open_module_contents (make_qualid [] (id_of_string s)); 
     m.module_opened <- true
   end
 
diff --git a/library/nametab.ml b/library/nametab.ml
index c8e10a1ed..046a9518c 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -17,22 +17,22 @@ let coq_root = "Coq"
 let default_root = "Scratch"
 
 (* Names tables *)
-type cci_table = global_reference Stringmap.t
-type obj_table = (section_path * obj) Stringmap.t
+type cci_table = global_reference Idmap.t
+type obj_table = (section_path * obj) Idmap.t
 type mod_table = (section_path * module_contents) Stringmap.t
 and module_contents = Closed of cci_table * obj_table * mod_table
 
 let empty =
-  Closed (Stringmap.empty, Stringmap.empty, Stringmap.empty)
+  Closed (Idmap.empty, Idmap.empty, Stringmap.empty)
  
 let persistent_nametab = ref (empty : module_contents)
 let local_nametab = ref (empty : module_contents)
 
 let push_cci (Closed (ccitab, objtab, modtab)) s ref =
-  Closed (Stringmap.add s ref ccitab, objtab, modtab)
+  Closed (Idmap.add s ref ccitab, objtab, modtab)
 
 let push_obj (Closed (ccitab, objtab, modtab)) s obj =
-  Closed (ccitab, Stringmap.add s obj objtab, modtab)
+  Closed (ccitab, Idmap.add s obj objtab, modtab)
 
 let push_mod (Closed (ccitab, objtab, modtab)) s mc =
   (* devrait pas mais ca plante en décommentant la ligne ci-dessous *)
@@ -78,6 +78,7 @@ let push_object sp obj =
 
 let push_module sp mc =
   let dir, s = repr_qualid (qualid_of_sp sp) in
+  let s = string_of_id s in
   push_mod_absolute dir s (sp,mc);
   if List.mem s !roots then 
     warning ("Cannot allow access to "^s^" by relative paths: it is already registered as a root of the Coq library")
@@ -86,7 +87,7 @@ let push_module sp mc =
 (* Sections are not accessible by basename *)
 let push_section sp mc =
   let dir, s = repr_qualid (qualid_of_sp sp) in
-  push_mod_absolute dir s (sp,mc)
+  push_mod_absolute dir (string_of_id s) (sp,mc)
 
 (* This is an entry point for local declarations at toplevel *)
 (* Do not use with "open" since it pushes an absolute name too *)
@@ -113,7 +114,7 @@ let locate qid =
   let (dir,id) = repr_qualid qid in
   let rec search (Closed (ccitab,_,modtab)) = function
     | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
-    | [] -> Stringmap.find id ccitab
+    | [] -> Idmap.find id ccitab
   in
   try search !local_nametab dir
   with Not_found -> search !persistent_nametab dir
@@ -122,16 +123,17 @@ let locate_obj qid =
   let (dir,id) = repr_qualid qid in
   let rec search (Closed (_,objtab,modtab)) = function
     | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
-    | [] -> Stringmap.find id objtab
+    | [] -> Idmap.find id objtab
   in
   try search !local_nametab dir
   with Not_found -> search !persistent_nametab dir
 
 let locate_module qid =
   let (dir,id) = repr_qualid qid in
+  let s = string_of_id id in
   let rec search (Closed (_,_,modtab)) = function
     | id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
-    | [] -> Stringmap.find id modtab
+    | [] -> Stringmap.find s modtab
   in
   try search !local_nametab dir
   with Not_found -> search !persistent_nametab dir
@@ -141,10 +143,10 @@ let locate_constant qid =
     | ConstRef sp -> sp
     | _ -> raise Not_found
 
-let sp_of_id _ id = locate (make_qualid [] (string_of_id id))
+let sp_of_id _ id = locate (make_qualid [] id)
 
 let constant_sp_of_id id =
-  match locate (make_qualid [] (string_of_id id)) with
+  match locate (make_qualid [] id) with
     | ConstRef sp -> sp
     | _ -> raise Not_found
 
@@ -160,7 +162,7 @@ let absolute_reference sp =
 exception Found of global_reference
 let locate_in_module dir id =
   let rec exists_in id (Closed (ccitab,_,modtab)) =
-    try raise (Found (Stringmap.find id ccitab))
+    try raise (Found (Idmap.find id ccitab))
     with Not_found -> 
       Stringmap.iter (fun _ (sp,mc) -> exists_in id mc) modtab
   in
@@ -174,28 +176,28 @@ let locate_in_module dir id =
 
 let locate_in_absolute_module dir id =
   check_absoluteness dir;
-  locate_in_module dir (string_of_id id)
+  locate_in_module dir id
 
 (* These are entry points to make the contents of a module/section visible *)
 (* in the current env (does not affect the absolute name space `coq_root') *)
 let open_module_contents qid =
   let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
-  Stringmap.iter push_cci_current ccitab;
-(*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
+  Idmap.iter push_cci_current ccitab;
+(*  Idmap.iter (fun _ -> Libobject.open_object) objtab;*)
   Stringmap.iter push_mod_current modtab
 
 let conditional_push ref = push_cci_current ref (* TODO *)
 
 let open_section_contents qid =
   let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
-  Stringmap.iter push_cci_current ccitab;
-(*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
+  Idmap.iter push_cci_current ccitab;
+(*  Idmap.iter (fun _ -> Libobject.open_object) objtab;*)
   Stringmap.iter push_mod_current modtab
 
 let rec rec_open_module_contents qid =
   let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
-  Stringmap.iter push_cci_current ccitab;
-(*  Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
+  Idmap.iter push_cci_current ccitab;
+(*  Idmap.iter (fun _ -> Libobject.open_object) objtab;*)
   Stringmap.iter 
     (fun m (sp,_ as mt) -> 
        push_mod_current m mt;
diff --git a/library/nametab.mli b/library/nametab.mli
index 08aea7ccc..a9a466bb3 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -10,8 +10,8 @@ open Term
 (* This module contains the table for globalization, which associates global
    names (section paths) to identifiers. *)
 
-type cci_table = global_reference Stringmap.t
-type obj_table = (section_path * Libobject.obj) Stringmap.t
+type cci_table = global_reference Idmap.t
+type obj_table = (section_path * Libobject.obj) Idmap.t
 type mod_table = (section_path * module_contents) Stringmap.t
 and module_contents = Closed of cci_table * obj_table * mod_table