diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-06-28 08:50:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-06-28 08:50:31 +0000 |
| commit | 066831b6390f36b818bb70e2f5cd606fb8a91d6f (patch) | |
| tree | ffb1a81b64dcb68b476a9c9dd43469d651083637 /kernel/indtypes.ml | |
| parent | a61a992cd460d11974676ad80e2362109d279a68 (diff) | |
Correction bug #983
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7176 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
| -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 5aee04f7d..afff821e4 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 |