diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-01-17 11:48:21 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-01-17 11:48:21 +0100 |
| commit | b3b229aae5df17272d0d1060da4795be5d2c9573 (patch) | |
| tree | 574d5af8b8f11ef0e099b9d7fb8504c638f070c8 /library/declaremods.ml | |
| parent | 20f9a1404f84ddabde2d1cbacc9063d9de87dfa9 (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/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 53f270701..cc7c4d7f1 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 |