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

1 files changed, 21 insertions, 19 deletions

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;