diff options
| author | coq | 2002-08-19 18:21:04 +0000 |
|---|---|---|
| committer | coq | 2002-08-19 18:21:04 +0000 |
| commit | 04dfb014ae67e1446aba386913131e18e6bbe41f (patch) | |
| tree | f36c281209313783b176473117f910f3818dd658 /kernel/subtyping.ml | |
| parent | f0591d4fdf4a39c53ee690fc7285b592161406de (diff) | |
La notation 'with'. L'interpretation - version preliminaire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index f62725c70d..fa024b7f25 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -182,12 +182,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 = c2 *) -let rec check_modules cst env msid1 l msb1 msb2 = +let rec check_modules cst env msid1 l + (mtb1,mpo1,cst1 as msb1) (mtb2,mpo2,cst2 as msb2) = let mp = (MPdot(MPself msid1,l)) in - let mty1 = strengthen env (fst msb1) mp in - let cst = check_modtypes cst env mty1 (fst msb2) false in + let mty1 = strengthen env mtb1 mp in + let cst = check_modtypes cst env mty1 mtb2 false in begin - match (snd msb1), (snd msb2) with + match mpo1, mpo2 with | _, None -> () | None, Some mp2 -> check_modpath_equiv env mp mp2 |