Prise en compte du repertoire dans le section path; utilisation de dirpath pour les noms de modules

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

3 files changed, 26 insertions, 9 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index ae80915b7..657a23ac3 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -167,11 +167,27 @@ let string_of_path sp =
   String.concat ""
     (List.flatten (List.map (fun s -> [s;"."]) (coq_root@sl))
      @ [ string_of_id id ])
+
+let parse_sp s =
+  let len = String.length s in
+  let rec decoupe_dirs n =
+    try
+      let pos = String.index_from s n '.' in
+      let dir = String.sub s n (pos-n) in
+      let dirs,n' = decoupe_dirs (succ pos) in
+      dir::dirs,n'
+    with
+      | Not_found -> [],n
+  in
+  if len = 0 then invalid_arg "parse_section_path";
+  let dirs,n = decoupe_dirs 0 in
+  let id = String.sub s n (len-n) in
+  dirs,id
     
 let path_of_string s =
   try
-    let (sl,s,k) = parse_section_path s in
-    make_path sl (id_of_string s) (kind_of_string k)
+    let sl,s = parse_sp s in
+    make_path sl (id_of_string s) CCI
   with
     | Invalid_argument _ -> invalid_arg "path_of_string"
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 76fc0b12a..4ea2ded00 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -16,7 +16,7 @@
 open Pp
 open Util
 
-type universe = { u_mod : string; u_num : int }
+type universe = { u_mod : Names.dir_path; u_num : int }
 
 let universe_ord x y =
   let c = x.u_num - y.u_num in
@@ -27,12 +27,13 @@ module UniverseOrdered = struct
   let compare = universe_ord
 end
 
-let pr_uni u = [< 'sTR u.u_mod ; 'sTR"." ; 'iNT u.u_num >]
+let pr_uni u =
+  [< 'sTR (Names.string_of_dirpath u.u_mod) ; 'sTR"." ; 'iNT u.u_num >]
 
-let dummy_univ = { u_mod = "dummy univ"; u_num = 0 } (* for prover terms *)
-let implicit_univ = { u_mod = "implicit univ"; u_num = 0 }
+let dummy_univ = { u_mod = ["dummy univ"]; u_num = 0 } (* for prover terms *)
+let implicit_univ = { u_mod = ["implicit univ"]; u_num = 0 }
 
-let current_module = ref ""
+let current_module = ref []
 
 let set_module m = current_module := m
 
@@ -68,7 +69,7 @@ let declare_univ u g =
 (* The universes of Prop and Set: Type_0, Type_1 and Type_2, and the
    resulting graph. *)
 let (initial_universes,prop_univ,prop_univ_univ,prop_univ_univ_univ) =
-  let prop_sp = "prop_univ" in
+  let prop_sp = ["prop_univ"] in
   let u = { u_mod = prop_sp; u_num = 0 } in
   let su = { u_mod = prop_sp; u_num = 1 } in
   let ssu = { u_mod = prop_sp; u_num = 2 } in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index c37ddba88..ba0b6aea1 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -16,7 +16,7 @@ val prop_univ : universe
 val prop_univ_univ : universe
 val prop_univ_univ_univ : universe
 
-val set_module : string -> unit
+val set_module : dir_path -> unit
 
 val new_univ : unit -> universe