Bug des locaux au premier niveau des modules qui disparaissaient de l'environnement (changement de is_section_p)

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

1 files changed, 13 insertions, 5 deletions

diff --git a/library/lib.ml b/library/lib.ml
index df48bc7cb..d0a015bd9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -29,14 +29,17 @@ and library_segment = library_entry list
 let lib_stk = ref ([] : (section_path * node) list)
 
 let module_name = ref None
-let path_prefix = ref (["Scratch"] : dir_path)
+let path_prefix = ref ([Nametab.default_root] : dir_path)
+
+let module_sp () =
+  match !module_name with Some m -> m | None -> [Nametab.default_root]
 
 let recalc_path_prefix () =
   let rec recalc = function
     | (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 -> ["Scratch"])
+    | [] -> module_sp ()
   in
   path_prefix := recalc !lib_stk
 
@@ -116,8 +119,10 @@ let check_for_module () =
   with Not_found -> ()
 
 let start_module s =
-  if !module_name <> None then error "a module is already started";
-  if !path_prefix <> ["Scratch"] then error "some sections are already opened";
+  if !module_name <> None then
+    error "a module is already started";
+  if !path_prefix <> [Nametab.default_root] then
+    error "some sections are already opened";
   module_name := Some s;
   Univ.set_module s;
   let _ = add_anonymous_entry (Module s) in
@@ -195,7 +200,10 @@ let reset_name id =
   in
   reset_to sp
 
-let is_section_p sp = dirpath_prefix_of sp !path_prefix
+(* [dir] is a section dir if [module] < [dir] <= [path_prefix] *)
+let is_section_p sp =
+  not (dirpath_prefix_of sp (module_sp ()))
+  & (dirpath_prefix_of sp !path_prefix)
 
 (* State and initialization. *)