From 066831b6390f36b818bb70e2f5cd606fb8a91d6f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 28 Jun 2005 08:50:31 +0000
Subject: Correction bug #983

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7176 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel')

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
-- 
cgit v1.2.3