Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 'section_path' pour les noms absolus

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

3 files changed, 36 insertions, 33 deletions

diff --git a/library/declare.mli b/library/declare.mli
index 95aa8be8f..388580a87 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -83,10 +83,10 @@ val extract_instance : global_reference -> constr array -> constr array
 val constr_of_reference :
   'a Evd.evar_map -> Environ.env -> global_reference -> constr
 
-val global_qualified_reference : section_path -> constr
+val global_qualified_reference : qualid -> constr
 val global_reference : path_kind -> identifier -> constr
 
-val construct_qualified_reference : Environ.env -> section_path -> constr
+val construct_qualified_reference : Environ.env -> qualid -> constr
 val construct_reference : Environ.env -> path_kind -> identifier -> constr
 
 val is_global : identifier -> bool
diff --git a/library/nametab.ml b/library/nametab.ml
index 8e15870e0..c45e7d93e 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -7,65 +7,66 @@ open Libobject
 open Declarations
 open Term
 
-type cci_table = global_reference Idmap.t
-type obj_table = (section_path * obj) Idmap.t
+type cci_table = global_reference Stringmap.t
+type obj_table = (section_path * obj) Stringmap.t
 type mod_table = module_contents Stringmap.t
 and module_contents = Closed of cci_table * obj_table * mod_table
 
 let mod_tab = ref (Stringmap.empty : mod_table)
-let cci_tab = ref (Idmap.empty : cci_table)
-let obj_tab = ref (Idmap.empty : obj_table)
+let cci_tab = ref (Stringmap.empty : cci_table)
+let obj_tab = ref (Stringmap.empty : obj_table)
 
-let sp_of_id _ id = Idmap.find id !cci_tab
+let sp_of_id _ id = Stringmap.find (string_of_id id) !cci_tab
 
 let constant_sp_of_id id =
-  match Idmap.find id !cci_tab with
+  match Stringmap.find (string_of_id id) !cci_tab with
     | ConstRef sp -> sp
     | _ -> raise Not_found
 
-let push_cci id sp = cci_tab := Idmap.add id sp !cci_tab
-let push_obj id sp = obj_tab := Idmap.add id sp !obj_tab
-let push_module id mc = mod_tab := Stringmap.add id mc !mod_tab
+let push_cci s sp = cci_tab := Stringmap.add s sp !cci_tab
+let push_obj s sp = obj_tab := Stringmap.add s sp !obj_tab
+let push_module s mc = mod_tab := Stringmap.add s mc !mod_tab
 
-let push = push_cci
+let push_object id = push_obj (string_of_id id)
+let push id = push_cci (string_of_id id) 
 
-let locate sp =
-  let (dir,id,_) = repr_path sp in
+let locate qid =
+  let (dir,id) = repr_qualid qid in
   let rec search (ccitab,modtab) = function
     | id :: dir' ->
 	let (Closed (ccitab, _, modtab)) = Stringmap.find id modtab in
 	search (ccitab,modtab) dir'
-    | [] -> Idmap.find id ccitab
+    | [] -> Stringmap.find id ccitab
   in search (!cci_tab,!mod_tab) dir
 
-let locate_obj sp =
-  let (dir,id,_) = repr_path sp in
+let locate_obj qid =
+  let (dir,id) = repr_qualid qid in
   let rec search (objtab,modtab) = function
     | id :: dir' ->
 	let (Closed (_, objtab, modtab)) = Stringmap.find id modtab in
 	search (objtab,modtab) dir'
-    | [] -> Idmap.find id objtab
+    | [] -> Stringmap.find id objtab
   in search (!obj_tab,!mod_tab) dir
 
-let locate_constant sp =
-  match locate sp with
+let locate_constant qid =
+  match locate qid with
     | ConstRef sp -> sp
     | _ -> raise Not_found
 
-let open_module_contents id =
-  let (Closed (ccitab,objtab,modtab)) = Stringmap.find id !mod_tab in
-  Idmap.iter push_cci ccitab;
-  Idmap.iter (fun _ -> Libobject.open_object) objtab;
+let open_module_contents s =
+  let (Closed (ccitab,objtab,modtab)) = Stringmap.find s !mod_tab in
+  Stringmap.iter push_cci ccitab;
+  Stringmap.iter (fun _ -> Libobject.open_object) objtab;
   Stringmap.iter push_module modtab
 
 (* Registration as a global table and roolback. *)
     
 let init () =
-  cci_tab := Idmap.empty;
-  obj_tab := Idmap.empty;
+  cci_tab := Stringmap.empty;
+  obj_tab := Stringmap.empty;
   mod_tab := Stringmap.empty;
 
-type frozen = cci_table Idmap.t * obj_table Idmap.t * mod_table Stringmap.t
+type frozen = cci_table Stringmap.t * obj_table Stringmap.t * mod_table Stringmap.t
 
 let freeze () = (!cci_tab, !obj_tab, !mod_tab)
 		  
diff --git a/library/nametab.mli b/library/nametab.mli
index 68e272740..9a90a70b8 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -10,13 +10,13 @@ open Term
 (* This module contains the table for globalization, which associates global
    names (section paths) to identifiers. *)
 
-type cci_table = global_reference Idmap.t
-type obj_table = (section_path * Libobject.obj) Idmap.t
+type cci_table = global_reference Stringmap.t
+type obj_table = (section_path * Libobject.obj) Stringmap.t
 type mod_table = module_contents Stringmap.t
 and module_contents = Closed of cci_table * obj_table * mod_table
 
 val push : identifier -> global_reference -> unit
-val push_obj : identifier -> (section_path * Libobject.obj) -> unit
+val push_object : identifier -> (section_path * Libobject.obj) -> unit
 val push_module : string -> module_contents -> unit
 
 val sp_of_id : path_kind -> identifier -> global_reference
@@ -24,9 +24,11 @@ val sp_of_id : path_kind -> identifier -> global_reference
 (* This returns the section path of a constant or fails with [Not_found] *)
 val constant_sp_of_id : identifier -> section_path
 
-val locate : section_path -> global_reference
-val locate_obj : section_path -> (section_path * Libobject.obj)
-val locate_constant : section_path -> constant_path
+val locate : qualid -> global_reference
+val locate_obj : qualid -> (section_path * Libobject.obj)
+val locate_constant : qualid -> constant_path
 
 val open_module_contents : string -> unit
 
+
+