diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5aee04f7d7..afff821e46 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -338,6 +338,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = match kind_of_term x with | Prod (na,b,d) -> assert (largs = []); + let b = whd_betadeltaiota env b in if not (noccur_between n ntypes b) then raise (IllFormedInd (LocalNonPos n)); check_pos (ienv_push_var ienv (na, b, mk_norec)) d |