From 0970c104868e62d580cce290790fe2a910f2c4c0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 17 Jun 2020 17:30:20 +0200
Subject: 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").
---
 kernel/safe_typing.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel')

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 }
-- 
cgit v1.2.3