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

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f3e2ac0f17..8b41ba0382 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -383,8 +383,11 @@ let vernac_declare_module id bl mty_ast_o mexpr_ast_o =
     Astmod.interp_module_decl evd env bl mty_ast_o mexpr_ast_o 
   in
   let argids, args = List.split arglist 
-  in (* We check the state of the system (in module, in module type)
-	and what parts are supplied *)
+  in (* We check the state of the system (in section, in module type)
+	and what module information is supplied *)
+    if Lib.sections_are_opened () then
+      error "Modules and Module Types are not allowed inside sections";
+
     match Lib.is_specification (), base_mty_o, base_mexpr_o with
       | _, None, None 
       | false, _, None ->
@@ -393,6 +396,7 @@ let vernac_declare_module id bl mty_ast_o mexpr_ast_o =
 	    ("Interactive Module "^ string_of_id id ^" started")
 	  
       | true, Some _, None
+      | true, _, Some (MEident _)
       | false, _, Some _ ->
 	  let mexpr_o = 
 	    option_app
@@ -416,7 +420,7 @@ let vernac_declare_module id bl mty_ast_o mexpr_ast_o =
 	    if_verbose message 
 	      ("Module "^ string_of_id id ^" is defined")
 
-      | true, _, Some _ ->
+      | true, _, Some (MEfunctor _ | MEapply _ | MEstruct _) ->
 	  error "Module definition not allowed in a Module Type"
 
 
@@ -434,15 +438,17 @@ let vernac_declare_module_type id bl mty_ast_o =
     Astmod.interp_module_decl evd env bl mty_ast_o None
   in
   let argids, args = List.split arglist 
-  in (* We check the state of the system (in module, in module type)
-	and what parts are supplied *)
-    match Lib.is_specification (), base_mty_o with
-      | _, None ->
+  in 
+    if Lib.sections_are_opened () then
+      error "Modules and Module Types are not allowed inside sections";
+
+    match base_mty_o with
+      | None ->
 	  Declaremods.start_modtype id argids args;
 	  if_verbose message 
 	    ("Interactive Module Type "^ string_of_id id ^" started")
 
-      | _, Some base_mty ->
+      | Some base_mty ->
 	  let mty = 
 	    List.fold_right 
 	      (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))