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

1 files changed, 11 insertions, 4 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 =