diff options
| author | soubiran | 2010-11-03 12:50:37 +0000 |
|---|---|---|
| committer | soubiran | 2010-11-03 12:50:37 +0000 |
| commit | f273a85429462e5c81b3e2b81a82f486fe1d94e2 (patch) | |
| tree | 65c6b6c5b39e82bc14dd847d74362f4f910d59d3 /kernel | |
| parent | 4ff5aea548076b6f0fd9ebca3cae0959681b35bb (diff) | |
Correction bug 2427
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13617 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/subtyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 12c760ac58..8e74ff7259 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -164,7 +164,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 match mind_of_delta reso2 kn2 with | kn2' when kn2=kn2' -> () | kn2' -> - if not (eq_mind (mind_of_delta reso1 kn1) kn2') then + if not (eq_mind (mind_of_delta reso1 kn1) (subst_ind subst2 kn2')) then error () end; (* we check that records and their field names are preserved. *) |