From e5cbf1ef44449f60eec3bb3c52d08b2943283279 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 30 Sep 2015 18:30:44 +0200 Subject: Univs: fix subtyping of polymorphic parameters. --- kernel/subtyping.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'kernel/subtyping.ml') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index db155e6c86..463e28a1c6 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -311,9 +311,12 @@ 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. *) + 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 Univ.check_constraints ctx1 (Environ.universes env) then cstrs, env, inst2 else error (IncompatibleConstraints ctx1) -- cgit v1.2.3 From d4869e059bfb73d99e1f5ef1b0a1f0906fa27056 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 15:40:17 +0200 Subject: Univs: correct handling of with in modules For polymorphic and non-polymorphic parameters and definitions, fixes bugs #4298, #4294 --- kernel/subtyping.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'kernel/subtyping.ml') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 463e28a1c6..58f3bcdf00 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 -- cgit v1.2.3 From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- kernel/subtyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/subtyping.ml') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 58f3bcdf00..a00a462e1b 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -317,7 +317,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = (* 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 + if UGraph.check_constraints ctx1 (Environ.universes env) then cstrs, env, inst2 else error (IncompatibleConstraints ctx1) with Univ.UniverseInconsistency incon -> -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/subtyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/subtyping.ml') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 58f3bcdf00..a422b18e00 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*