diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-26 16:22:35 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-26 16:22:35 +0000 |
| commit | 2c8ad1f81c486115fad58553ed15e775ca50de87 (patch) | |
| tree | 5c2c4ef953ffdf7876ee8618b8bae713b7016a95 /checker/subtyping.ml | |
| parent | cf21be5bfd42720bd1cc8756cfcdb388cdaebd80 (diff) | |
Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)
When doing a [check_subtypes env mtb1 mtb2], we used to always add [mtb1]
in the environment. But since the stricter checks of commit r14150, this
is an error if the environment already knows [mtb1] (for instance
when doing (F M) and checking that M is compatible with the type of the
arg of F.
[check_subtypes] now expect [mtb1] to be already in env, and we move the
add_module to the unique call site of this function that requires it.
Moreover, we solve a second issue : when subtyping a functor, we
update the environment once inside the functor, and this is also
refused by the checks of commits r14150. So we first remove the module
name from the env before doing the update. Since the module added
earlier was a functor, there is no inner defs to chase in env.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14615 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/subtyping.ml')
| -rw-r--r-- | checker/subtyping.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 0603300ba..0c97254b5 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -348,7 +348,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; @@ -367,8 +368,5 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = else check_structure env mtb1' mtb2' equiv subst1 subst2 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 sup sup.typ_mp) super empty_subst (map_mp super.typ_mp sup.typ_mp) false |