summaryrefslogtreecommitdiff
path: root/checker/subtyping.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
commit300293c119981054c95182a90c829058530a6b6f (patch)
treed7303613741c5796b58ced7db24ec7203327dbb2 /checker/subtyping.ml
parent9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff)
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'checker/subtyping.ml')
-rw-r--r--checker/subtyping.ml15
1 files changed, 7 insertions, 8 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -280,8 +280,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
| _ -> 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*)