diff options
| author | Pierre Courtieu | 2016-04-15 16:45:14 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2016-04-15 16:45:14 +0200 |
| commit | caa1f67de10614984fa7e1c68aa8adf0ff90196a (patch) | |
| tree | 3c265ac5e16851c5dc1ca917ddb03725e09ea0ff /kernel/subtyping.ml | |
| parent | be824224cc76f729872e9d803fc64831b95aee94 (diff) | |
| parent | 3b3d98acd58e91c960a2e11cd47ac19b2b34f86b (diff) | |
Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index db155e6c86..5efc1078ee 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -311,15 +311,19 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = try (* The environment with the expected universes plus equality of the body instances with the expected instance *) - let env = Environ.add_constraints cstrs env in - (* Check that the given definition does not add any constraint over - the expected ones, so that it can be used in place of the original. *) - if Univ.check_constraints ctx1 (Environ.universes env) then + let ctxi = Univ.Instance.append inst1 inst2 in + let ctx = Univ.UContext.make (ctxi, cstrs) in + let env = Environ.push_context ctx env in + (* Check that the given definition does not add any constraint over + the expected ones, so that it can be used in place of + the original. *) + if UGraph.check_constraints ctx1 (Environ.universes env) then cstrs, env, inst2 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 @@ -456,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 |