diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
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 } |