From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 25 Dec 2011 13:19:42 +0100 Subject: Imported Upstream version 8.3.pl3 --- checker/subtyping.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'checker/subtyping.ml') diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 684a59ad..4f113cf9 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* error () let rec check_modules env msb1 msb2 subst1 subst2 = - let mty1 = module_type_of_module env None msb1 in - let mty2 = module_type_of_module env None msb2 in + let mty1 = module_type_of_module None msb1 in + let mty2 = module_type_of_module None msb2 in check_modtypes env mty1 mty2 subst1 subst2 false; @@ -343,7 +343,8 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = (module_body_of_type (MPbound arg_id2) arg_t2) env in let env = match body_t1 with - SEBstruct str -> + SEBstruct str -> + let env = shallow_remove_module mtb1.typ_mp env in add_module {mod_mp = mtb1.typ_mp; mod_expr = None; mod_type = body_t1; @@ -363,10 +364,8 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = let check_subtypes env sup super = (*if sup<>super then*) - let env = add_module - (module_body_of_type sup.typ_mp sup) env in - check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst - (map_mp super.typ_mp sup.typ_mp) false + check_modtypes env (strengthen sup sup.typ_mp) super empty_subst + (map_mp super.typ_mp sup.typ_mp) false let check_equal env sup super = (*if sup<>super then*) -- cgit v1.2.3