diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -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 00af99d980..c141a02aa3 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -163,7 +163,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* the inductive types and constructors types have to be convertible *) check (fun mib -> mib.mind_nparams) (fun x -> InductiveParamsNumberField x); - begin + begin match mind_of_delta reso2 kn2 with | kn2' when kn2=kn2' -> () | kn2' -> |