diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-05 16:03:47 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-11 11:04:45 +0100 |
| commit | 0cd0a3ecdc7f942da153c59369ca3572bd18dd10 (patch) | |
| tree | bc0da893f040205068263f3133f9793cdf405b06 /kernel/safe_typing.ml | |
| parent | 64867e7f6a86867e45ddd052b82f51b1b0355c97 (diff) | |
Fix (3243): univ constraints of module subtyping were not propagated
Universe constraints coming from subtyping were not propagated
to the outermost module and hence not stocked in the .vo file.
Still, they were added to the interactive safe environment and
hence checked for satisfiability.
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bf758b96b..867705c47 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -557,7 +557,10 @@ let end_module l restype senv = let mb = build_module_body params restype senv in let newenv = oldsenv.env in let newenv = set_engagement_opt newenv senv.engagement in - let senv'= propagate_loads {senv with env=newenv} in + let senv'= + propagate_loads { senv with + env = newenv; + univ = Univ.union_constraints senv.univ mb.mod_constraints} in let newenv = Environ.add_constraints mb.mod_constraints senv'.env in let newenv = Modops.add_module mb newenv in let newresolver = |