diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a5224914b..6ea71e09a 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -337,8 +337,11 @@ let listrec_mconstr env ntypes hyps nparams i indlc = else raise (IllFormedInd (LocalNonPos n)) | Ind ind_sp -> - if List.for_all (noccur_between n ntypes) largs - then Norec + (* If the inductive type being defined or a parameter appears as + parameter, then we have an imbricated type *) + if List.for_all (noccur_between n ntypes) largs && + List.for_all (noccur_between (n-nhyps) nhyps) largs + then Norec else Imbr(ind_sp,imbr_positive env n ind_sp largs) | err -> if noccur_between n ntypes x && |