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 /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions