diff options
| author | Pierre-Marie Pédrot | 2020-10-07 18:28:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-09 11:34:10 +0200 |
| commit | 32e26090369e47e3e83e4313b3eefb321bc3311e (patch) | |
| tree | 3f46b52c379454a9e67201d39bea3106a7b281ad /kernel/type_errors.ml | |
| parent | e85f6b36711bf7214b2351724ea56b7808ab2321 (diff) | |
Store the resolver of required modules as functor parameters in safe_env.
The safe environment features two different sets of delta resolvers, one for
module parameters and one for the actual body of the module being built. The
purpose of this separations seems to have been to reduce the number of name
equations being added to the environment, since the one from the parameters
would already be present at instanciation time.
Semantically, required modules behave like parameters in this respect, i.e.
delta resolvers that come from modules dependend upon are guaranteed to be added
when that module is actually required. As such, there is no need to store the
quotient coming from the dependencies inside the vo file of a given library.
Yet, the previous code would precisely do that, leading to a potential quadratic
blowup in vo file size, similarly to the issue with vio files storing the whole
chain of dependency. This patch fixes the issue simply by segregating those
redundant constraints in the dedicated field, thus dropping them from the vo.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions
