aboutsummaryrefslogtreecommitdiff
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 93337fca5d..8b85072d6d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1023,6 +1023,8 @@ let start_module l senv =
mp,
{ empty_environment with
env = senv.env;
+ modresolver = senv.modresolver;
+ paramresolver = senv.paramresolver;
modpath = mp;
modvariant = STRUCT ([],senv);
required = senv.required }
@@ -1034,6 +1036,8 @@ let start_modtype l senv =
mp,
{ empty_environment with
env = senv.env;
+ modresolver = senv.modresolver;
+ paramresolver = senv.paramresolver;
modpath = mp;
modvariant = SIG ([], senv);
required = senv.required }