diff options
| author | coqbot-app[bot] | 2020-10-12 16:35:23 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-12 16:35:23 +0000 |
| commit | 07a199ffa640b9eb94235ebc3732c4b2981ca525 (patch) | |
| tree | ad166ce5fb96f3c2e02e5998312ebac779bb4ab9 | |
| parent | 2ff70d8341177d384043dd3d02da6968a8788e32 (diff) | |
| parent | 32e26090369e47e3e83e4313b3eefb321bc3311e (diff) | |
Merge PR #13156: Store the resolver of required modules as functor parameters in safe_env
Reviewed-by: herbelin
| -rw-r--r-- | kernel/safe_typing.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index da77a2882e..3dee3d2b2f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -79,8 +79,10 @@ module NamedDecl = Context.Named.Declaration * STRUCT (params,oldsenv) : inside a local module, with module parameters [params] and earlier environment [oldsenv] * SIG (params,oldsenv) : same for a local module type - - [modresolver] : delta_resolver concerning the module content - - [paramresolver] : delta_resolver concerning the module parameters + - [modresolver] : delta_resolver concerning the module content, that needs to + be marshalled on disk + - [paramresolver] : delta_resolver in scope but not part of the library per + se, that is from functor parameters and required libraries - [revstruct] : current module content, most recent declarations first - [modlabels] and [objlabels] : names defined in the current module, either for modules/modtypes or for constants/inductives. @@ -1301,7 +1303,9 @@ let import lib cst vodigest senv = mp, { senv with env; - modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver; + (* Do NOT store the name quotient from the dependencies in the set of + constraints that will be marshalled on disk. *) + paramresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.paramresolver; required = DPmap.add lib.comp_name vodigest senv.required; loads = (mp,mb)::senv.loads; sections; |