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, 8 insertions, 7 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 4dd0a36f2..a7028e120 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -8,7 +8,7 @@ open Summary
 
 type node = 
   | Leaf of obj
-  | Module of string
+  | Module of dir_path
   | OpenedSection of string * Summary.frozen
   (* bool is to tell if the section must be opened automatically *)
   | ClosedSection of bool * string * library_segment
@@ -36,7 +36,7 @@ let recalc_path_prefix () =
     | (sp, OpenedSection _) :: _ ->
 	let (pl,id,_) = repr_path sp in pl@[string_of_id id]
     | _::l -> recalc l
-    | [] -> (match !module_name with Some m -> [m] | None -> [])
+    | [] -> (match !module_name with Some m -> m | None -> [])
   in
   path_prefix := recalc !lib_stk
 
@@ -120,7 +120,7 @@ let start_module s =
   module_name := Some s;
   Univ.set_module s;
   let _ = add_anonymous_entry (Module s) in
-  path_prefix := [s]
+  path_prefix := s
 
 let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
@@ -198,7 +198,7 @@ let is_section_p sp = dirpath_prefix_of sp !path_prefix
 
 (* State and initialization. *)
 
-type frozen = string option * library_segment
+type frozen = dir_path option * library_segment
 
 let freeze () = (!module_name, !lib_stk)
 
diff --git a/library/lib.mli b/library/lib.mli
index 35d8cf2ac..ed08bcc1d 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -13,7 +13,7 @@ open Summary
 
 type node = 
   | Leaf of obj
-  | Module of string
+  | Module of dir_path
   | OpenedSection of string * Summary.frozen
   | ClosedSection of bool * string * library_segment
   | FrozenState of Summary.frozen
@@ -47,7 +47,7 @@ val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> dir_path
 val is_section_p : dir_path -> bool
 
-val start_module : string -> unit
+val start_module : dir_path -> unit
 val export_module : unit -> library_segment
 
 
diff --git a/library/library.ml b/library/library.ml
index b9f1b109a..cd99b603e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -159,7 +159,8 @@ let rec load_module_from s f =
     List.iter (load_mandatory_module s) m.module_deps;
     Global.import m.module_compiled_env;
     load_objects m.module_declarations;
-    let sp = Names.make_path [] (id_of_string s) CCI in
+    let dir = parse_loadpath lpe.relative_subdir in
+    let sp = Names.make_path dir (id_of_string s) CCI in
     Nametab.push_module sp m.module_nametab;
     modules_table := Stringmap.add s m !modules_table;
     m