diff options
| author | Hugo Herbelin | 2020-06-17 17:30:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-08 10:22:07 +0200 |
| commit | 0970c104868e62d580cce290790fe2a910f2c4c0 (patch) | |
| tree | b9dc9b8ff14c22e797f9776ac460db35bdbd43e1 /kernel | |
| parent | 827425e57f9ecb9bbff3132bdaa504e710c8cf2b (diff) | |
Preserve delta-resolver at Module and Module Type starting.
The default value of the delta-resolver for name aliasing was
reinitialized at Module and Module Type starting time. The existing
resolver was saved but the saved value was not used in
Safe_typing.constant_of_delta_kn_senv and
Safe_typing.mind_of_delta_kn_senv.
A possible fix could have been to take the saved resolver into account
in Safe_typing.constant_of_delta_kn_senv and
Safe_typing.mind_of_delta_kn_senv. We just try instead not to
reinitialize it.
This incidentally fixes #12525 (Search unable to see through an
"Include" when in an ongoing "Module").
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 } |