Forbid Require inside interactive modules and module types.

Fixes #3379 and part of #3363. Also avoids fragile code propagating required
libraries when closing an interactive module.

Had to fix a few occurrences in std lib.

1 files changed, 6 insertions, 16 deletions

diff --git a/library/library.ml b/library/library.ml
index 343588652..20fc31961 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -533,18 +533,12 @@ let in_require : require_obj -> obj =
    if [export = Some true] *)
 
 let require_library_from_dirpath modrefl export =
+  if Lib.is_module_or_modtype () then
+    error "Require is not allowed inside a module or a module type";
   let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
   let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
   let modrefl = List.map fst modrefl in
-    if Lib.is_module_or_modtype () then
-      begin
-	add_anonymous_leaf (in_require (needed,modrefl,None));
-	Option.iter (fun exp ->
-	  List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
-	  export
-      end
-    else
-      add_anonymous_leaf (in_require (needed,modrefl,export));
+  add_anonymous_leaf (in_require (needed,modrefl,export));
   add_frozen_state ()
 
 let require_library qidl export =
@@ -552,15 +546,11 @@ let require_library qidl export =
     require_library_from_dirpath modrefl export
 
 let require_library_from_file idopt file export =
+  if Lib.is_module_or_modtype () then
+    error "Require is not allowed inside a module or a module type";
   let modref,needed = rec_intern_library_from_file idopt file in
   let needed = List.rev_map snd needed in
-  if Lib.is_module_or_modtype () then begin
-    add_anonymous_leaf (in_require (needed,[modref],None));
-    Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
-      export
-  end
-  else
-    add_anonymous_leaf (in_require (needed,[modref],export));
+  add_anonymous_leaf (in_require (needed,[modref],export));
   add_frozen_state ()
 
 (* the function called by Vernacentries.vernac_import *)