diff options
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. *) |