diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 16:28:45 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 16:28:45 +0000 |
| commit | 28809ba4180b0421d5b0e97f9e92ba72e63bda7c (patch) | |
| tree | 5c80ee58097dd01b2ecd420eab95a567dc274005 /checker/subtyping.ml | |
| parent | ccba6c718af6a5a15f278fc9365b6ad27108e98f (diff) | |
After the approval of Bruno, here the patch for the checker.
In checker:
- delta_resolver inferred by the module system is checked through regular delta reduction steps
- the old mind_equiv field of mutual_inductive is simulated through a special table in environ
- small optimization, if the signature and the implementation of a module are physically equal
(always happen for the toplevel module of a vo) then the checker checks only the signature.
In kernel
- in names i have added two special equality functions over constant and inductive names for the checker,
so that the checker does not take in account the cannonical name inferred by the module system.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12977 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/subtyping.ml')
| -rw-r--r-- | checker/subtyping.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 9df49630c..d66a49546 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -361,8 +361,10 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = let check_subtypes env sup super = (*if sup<>super then*) - check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst - (map_mp super.typ_mp sup.typ_mp) false + 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 let check_equal env sup super = (*if sup<>super then*) |