diff options
| author | Gaëtan Gilbert | 2020-07-10 13:07:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-10 13:07:21 +0200 |
| commit | f2dc2f5fc8c745c69c0161a91063b11838fb684b (patch) | |
| tree | 0127fb4a562a4a56af12a4bef332705562996f2d /kernel | |
| parent | 9b4d89c5376e8018ca94bc3bd877f99f1d03ec74 (diff) | |
| parent | 0046a166843495b131fb197788c28de9b4705685 (diff) | |
Merge PR #12537: Take into account the existing delta-resolver when starting a new interactive module or module type
Reviewed-by: SkySkimmer
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 } |