Strengthenning rules for modules + No modules in sections

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

4 files changed, 15 insertions, 9 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 7b5adfdc9..89a826c92 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -403,7 +403,8 @@ let start_module id argids args res_o =
   let fs = Summary.freeze_summaries () in
     process_module_bindings argids args;
     openmod_info:=(mbids,res_o);
-    Lib.start_module id mp fs;
+    let prefix = Lib.start_module id mp fs in
+    Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
     Lib.add_frozen_state ()
 
 
@@ -515,7 +516,8 @@ let start_modtype id argids args =
   let fs= Summary.freeze_summaries () in
     process_module_bindings argids args;
     openmodtype_info := (List.map fst args);
-    Lib.start_modtype id mp fs;
+    let prefix = Lib.start_modtype id mp fs in
+    Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
     Lib.add_frozen_state ()
 
 
diff --git a/library/lib.ml b/library/lib.ml
index 286133305..323ca60de 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -268,7 +268,8 @@ let start_module id mp nametab =
   if Nametab.exists_module dir then
     errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
   add_entry oname (OpenedModule (prefix,nametab));
-  path_prefix := prefix
+  path_prefix := prefix;
+  prefix
 (*  add_frozen_state () must be called in declaremods *)
  
 let end_module id = 
@@ -303,7 +304,8 @@ let start_modtype id mp nametab =
   if Nametab.exists_cci sp then
     errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ;
   add_entry name (OpenedModtype (prefix,nametab));
-  path_prefix := prefix
+  path_prefix := prefix;
+  prefix
 
 let end_modtype id = 
   let sp,nametab = 
diff --git a/library/lib.mli b/library/lib.mli
index 90f111c4b..075be2890 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -123,11 +123,13 @@ val module_dp : unit -> dir_path
 
 (*s Modules and module types *)
 
-val start_module : module_ident -> module_path -> Summary.frozen -> unit
+val start_module : 
+  module_ident -> module_path -> Summary.frozen -> object_prefix
 val end_module : module_ident 
   -> object_name * object_prefix * Summary.frozen * library_segment
 
-val start_modtype : module_ident -> module_path -> Summary.frozen -> unit
+val start_modtype : 
+  module_ident -> module_path -> Summary.frozen -> object_prefix
 val end_modtype : module_ident 
   -> object_name * object_prefix * Summary.frozen * library_segment
 
diff --git a/library/nametab.ml b/library/nametab.ml
index bc419a237..1f8111a2c 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -106,7 +106,7 @@ let push_many vis tab dir o =
 	      | Absolute _ -> 
             (* This is an absolute name, we must keep it otherwise it may
                become unaccessible forever *)
-		  warning "Trying to zaslonic an absolute name!"; current
+		  warning "Trying to mask an absolute name!"; current
 	      | Nothing
 	      | Relative _ -> Relative o
           else current 
@@ -118,7 +118,7 @@ let push_many vis tab dir o =
               (* This is an absolute name, we must keep it otherwise it may
 		 become unaccessible forever *)
 	      (* But ours is also absolute! This is an error! *)
-	      error "Trying to zaslonic an absolute name!"
+	      error "Trying to mask an absolute name!"
 	  | Nothing
 	  | Relative _ -> Absolute o, dirmap
   in
@@ -137,7 +137,7 @@ let push_one vis tab dir o =
 		| Absolute _ -> 
 	(* This is an absolute name, we must keep it otherwise it may
            become unaccessible forever *)
-		    error "Trying to zaslonic an absolute name!"
+		    error "Trying to mask an absolute name!"
 		| Nothing
 		| Relative _ -> Relative o
 	    in