Imported Upstream version 8.0pl3upstream/8.0pl3

1 files changed, 23 insertions, 11 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 88f837aa..0b1d49f5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml,v 1.59.2.1 2004/07/16 19:30:25 herbelin Exp $ *)
+(* $Id: indtypes.ml,v 1.59.2.4 2005/12/30 15:58:59 barras Exp $ *)
 
 open Util
 open Names
@@ -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            *)
@@ -46,6 +50,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
@@ -337,9 +346,10 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
     match kind_of_term x with
       | Prod (na,b,d) ->
 	  assert (largs = []);
-          if not (noccur_between n ntypes b) then
-	    raise (IllFormedInd (LocalNonPos n));
-	  check_pos (ienv_push_var ienv (na, b, mk_norec)) 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)) d)
       | Rel k ->
           let (ra,rarg) =
             try List.nth ra_env (k-1)
@@ -481,7 +491,7 @@ let allowed_sorts env issmall isunit = function
         then logical_sorts else impredicative_sorts
       else logical_sorts
 
-let build_inductive env env_ar finite inds recargs cst =
+let build_inductive env env_ar record finite inds recargs cst =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let ids = 
@@ -527,7 +537,8 @@ let build_inductive env env_ar finite inds recargs cst =
     } in
   let packets = array_map2 build_one_packet inds recargs in
   (* Build the mutual inductive *)
-  { mind_ntypes = ntypes;
+  { mind_record = record;
+    mind_ntypes = ntypes;
     mind_finite = finite;
     mind_hyps = hyps;
     mind_packets = packets;
@@ -544,5 +555,6 @@ let check_inductive env mie =
   (* Then check positivity conditions *)
   let recargs = check_positivity env_arities inds in
   (* Build the inductive packets *)
-  build_inductive env env_arities mie.mind_entry_finite inds recargs cst
+  build_inductive env env_arities mie.mind_entry_record mie.mind_entry_finite 
+    inds recargs cst