aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-10-07 18:28:50 +0200
committerPierre-Marie Pédrot2020-10-09 11:34:10 +0200
commit32e26090369e47e3e83e4313b3eefb321bc3311e (patch)
tree3f46b52c379454a9e67201d39bea3106a7b281ad /kernel/nativelambda.mli
parente85f6b36711bf7214b2351724ea56b7808ab2321 (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/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions