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

1 files changed, 4 insertions, 2 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 7b5adfdc98..89a826c925 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 ()