diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-01 15:40:17 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:13 +0200 |
| commit | d4869e059bfb73d99e1f5ef1b0a1f0906fa27056 (patch) | |
| tree | 7423c05712096bd870f3985eaad94d5daefeea72 /kernel/subtyping.ml | |
| parent | 90a2126b2fb2738a7684864e74e0d1ed3c861a98 (diff) | |
Univs: correct handling of with in modules
For polymorphic and non-polymorphic parameters and definitions, fixes
bugs #4298, #4294
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 463e28a1c..58f3bcdf0 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -322,7 +322,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = else error (IncompatibleConstraints ctx1) with Univ.UniverseInconsistency incon -> error (IncompatibleUniverses incon) - else cst, env, Univ.Instance.empty + else + cst, env, Univ.Instance.empty in (* Now check types *) let typ1 = Typeops.type_of_constant_type env' cb1.const_type in @@ -459,6 +460,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = let check_subtypes env sup super = let env = add_module_type sup.mod_mp sup env in + let env = Environ.push_context_set ~strict:true super.mod_constraints env in check_modtypes Univ.Constraint.empty env (strengthen sup sup.mod_mp) super empty_subst (map_mp super.mod_mp sup.mod_mp sup.mod_delta) false |