From d3f6e92fc69b5b64681cff285ab964b69cef5819 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 20 Jan 2006 16:35:03 +0000
Subject: *** empty log message ***

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

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 83928b6cca..643dd4da2a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -20,10 +20,14 @@ open Reduction
 open Typeops
 open Entries
 
-(* [check_constructors_names id s cl] checks that all the constructors names
-   appearing in [l] are not present in the set [s], and returns the new set
-   of names. The name [id] is the name of the current inductive type, used
-   when reporting the error. *)
+(* Same as noccur_between but may perform reductions.
+   Could be refined more...  *)
+let weaker_noccur_between env x nvars t =
+  if noccur_between x nvars t then Some t
+  else
+   let t' = whd_betadeltaiota env t in
+   if noccur_between x nvars t' then Some t'
+   else None
 
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
@@ -42,6 +46,11 @@ type inductive_error =
 
 exception InductiveError of inductive_error
 
+(* [check_constructors_names id s cl] checks that all the constructors names
+   appearing in [l] are not present in the set [s], and returns the new set
+   of names. The name [id] is the name of the current inductive type, used
+   when reporting the error. *)
+
 let check_constructors_names id =
   let rec check idset = function
     | [] -> idset
@@ -357,10 +366,10 @@ 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)) nmr d
+          (match weaker_noccur_between env n ntypes b with
+              None -> raise (IllFormedInd (LocalNonPos n));
+            | Some b ->
+	        check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
       | Rel k ->
            (try let (ra,rarg) = List.nth ra_env (k-1) in 
 		let nmr1 =
-- 
cgit v1.2.3