Prise en compte de noms absolus dans la nametab

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

2 files changed, 22 insertions, 12 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index c8eb17ca9..ae80915b7 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -136,10 +136,14 @@ let repr_qualid q = q
 let string_of_qualid (l,s) = String.concat "." (l@[s])
 let pr_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s])
 
-(*s Section paths *)
-
+(*s Directory paths = section names paths *)
 type dir_path = string list
 
+(* The root of absolute names *)
+let coq_root = ["Coq"]
+
+(*s Section paths are absolute names *)
+
 type section_path = {
   dirpath : dir_path ;
   basename : identifier ;
@@ -152,13 +156,16 @@ let kind_of_path sp = sp.kind
 let basename sp = sp.basename
 let dirpath sp = sp.dirpath
 
+let qualid_of_sp sp =
+  make_qualid (coq_root @ dirpath sp) (string_of_id (basename sp))
+
 (* parsing and printing of section paths *)
-let string_of_dirpath sl = String.concat "#" (""::sl)
+let string_of_dirpath sl = String.concat "." (coq_root@sl)
 
 let string_of_path sp =
   let (sl,id,k) = repr_path sp in
   String.concat ""
-    ("#"::(List.flatten (List.map (fun s -> [s;"."]) sl))
+    (List.flatten (List.map (fun s -> [s;"."]) (coq_root@sl))
      @ [ string_of_id id ])
     
 let path_of_string s =
diff --git a/kernel/names.mli b/kernel/names.mli
index 070e7917f..a5ae56da4 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -46,21 +46,21 @@ val kind_of_string : string -> path_kind
 (*s Directory paths = section names paths *)
 type dir_path = string list
 
-(* Printing of directory paths as ["#module#submodule"] *)
-val string_of_dirpath : dir_path -> string
-
+val coq_root : dir_path
 
-(*s Section paths *)
+(* Printing of directory paths as ["coq_root.module.submodule"] *)
+val string_of_dirpath : dir_path -> string
 
+(*s Qualified idents are names relative to the current visilibity of names *)
 type qualid
 
-val make_qualid : string list -> string -> qualid
-val repr_qualid : qualid -> string list * string
+val make_qualid : dir_path -> string -> qualid
+val repr_qualid : qualid -> dir_path * string
 
 val string_of_qualid : qualid -> string
 val pr_qualid : qualid -> std_ppcmds
 
-(*s Section paths *)
+(*s Section paths are {\em absolute} names *)
 type section_path
 
 (* Constructors of [section_path] *)
@@ -75,7 +75,10 @@ val kind_of_path : section_path -> path_kind
 val sp_of_wd : string list -> section_path
 val wd_of_sp : section_path -> string list
 
-(* Parsing and printing of section path as ["#module#id#kind"] *)
+(* Turns an absolute name into a qualified name denoting the same name *)
+val qualid_of_sp : section_path -> qualid
+
+(* Parsing and printing of section path as ["coq_root.module.id"] *)
 val path_of_string : string -> section_path
 val string_of_path : section_path -> string
 val pr_sp : section_path -> std_ppcmds