From 0cd0a3ecdc7f942da153c59369ca3572bd18dd10 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 5 Mar 2014 16:03:47 +0100 Subject: 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. --- kernel/safe_typing.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel') 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 = -- cgit v1.2.3