diff options
| author | Maxime Dénès | 2015-01-17 11:48:21 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:16:44 +0530 |
| commit | d187edf437ca4dac73b1da5d434cdf164c129319 (patch) | |
| tree | e659a1e577e9281aa6507fea520fd94c9c57009b /library | |
| parent | 18ac6441e93ca670740a1b874033ec016d4f1392 (diff) | |
Partially revert "Forbid Require inside interactive modules and module types."
This reverts commit 6d5b56d971506dfadcfc824bfbb09dc21718e42b but does not put
back in place the Requires inside modules that were found in the std lib.
Conflicts:
kernel/safe_typing.ml
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 1 | ||||
| -rw-r--r-- | library/library.ml | 22 |
2 files changed, 16 insertions, 7 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 53f270701c..cc7c4d7f11 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -850,7 +850,6 @@ let library_values = Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES" let register_library dir cenv (objs:library_objects) digest univ = - assert (not (Lib.is_module_or_modtype ())); let mp = MPfile dir in let () = try diff --git a/library/library.ml b/library/library.ml index b443c2a4c7..481d8707a9 100644 --- a/library/library.ml +++ b/library/library.ml @@ -537,12 +537,18 @@ 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 - add_anonymous_leaf (in_require (needed,modrefl,export)); + 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_frozen_state () let require_library qidl export = @@ -550,11 +556,15 @@ 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 - add_anonymous_leaf (in_require (needed,[modref],export)); + 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_frozen_state () (* the function called by Vernacentries.vernac_import *) |