Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 271 insertions, 304 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 736f4da1..d9f9f912 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductive.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
+(* $Id: inductive.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
 
 open Util
 open Names
@@ -47,6 +47,8 @@ let find_coinductive env c =
         when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
     | _ -> raise Not_found
 
+let inductive_params (mib,_) = mib.mind_nparams
+
 (************************************************************************)
 
 (* Build the substitution that replaces Rels by the appropriate *)
@@ -80,10 +82,12 @@ let instantiate_params full t args sign =
 
 let instantiate_partial_params = instantiate_params false
 
-let full_inductive_instantiate mib params t =
-  instantiate_params true t params mib.mind_params_ctxt
+let full_inductive_instantiate mib params sign =
+  let dummy = mk_Prop in
+  let t = mkArity (sign,dummy) in
+  fst (destArity (instantiate_params true t params mib.mind_params_ctxt))
 
-let full_constructor_instantiate (((mind,_),mib,_),params) =
+let full_constructor_instantiate ((mind,_),(mib,_),params) =
   let inst_ind = constructor_instantiate mind mib in
   (fun t ->
     instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
@@ -93,22 +97,6 @@ let full_constructor_instantiate (((mind,_),mib,_),params) =
 
 (* Functions to build standard types related to inductive *)
 
-(* For each inductive type of a block that is of level u_i, we have
-   the constraints that u_i >= v_i where v_i is the type level of the
-   types of the constructors of this inductive type. Each v_i depends
-   of some of the u_i and of an extra (maybe non variable) universe,
-   say w_i. Typically, for three inductive types, we could have
-
-   u1,u2,u3,w1 <= u1
-   u1       w2 <= u2
-      u2,u3,w3 <= u3
-
-   From this system of inequations, we shall deduce
-
-   w1,w2,w3 <= u1
-   w1,w2 <= u2
-   w1,w2,w3 <= u3
-*)   
 
 let number_of_inductives mib = Array.length mib.mind_packets
 let number_of_constructors mip = Array.length mip.mind_consnames
@@ -134,17 +122,6 @@ where
 Remark: Set (predicative) is encoded as Type(0)
 *)
 
-let find_constraint levels level_bounds i nci =
-  if nci = 0 then mk_Prop
-  else
-    let level_bounds' = solve_constraints_system levels level_bounds in
-    let level = level_bounds'.(i) in
-    if nci = 1 & is_empty_universe level then mk_Prop
-    else if Univ.is_base level then mk_Set else Type level
-
-let find_inductive_level env (mib,mip) (_,i) levels level_bounds =
-  find_constraint levels level_bounds i (number_of_constructors mip)
-
 let set_inductive_level env s t = 
   let sign,s' = dest_prod_assum env t in
   if family_of_sort s <> family_of_sort (destSort s') then
@@ -153,45 +130,69 @@ let set_inductive_level env s t =
   else
     t
 
-let constructor_instances env (mib,mip) (_,i) args =
-  let nargs = Array.length args in
-  let args = Array.to_list args in
-  let uargs = 
-    if nargs > mib.mind_nparams_rec then
-      fst (list_chop mib.mind_nparams_rec args)
-    else args in
-  let arities =
-    Array.map (fun mip -> destArity mip.mind_nf_arity) mib.mind_packets in
-  (* Compute the minimal type *)
-  let levels = Array.init 
-    (number_of_inductives mib) (fun _ -> fresh_local_univ ()) in
-  let arities = list_tabulate (fun i -> 
-    let ctx,s = arities.(i) in
-    let s = match s with Type _ -> Type (levels.(i)) | s -> s in
-    (Name mib.mind_packets.(i).mind_typename,None,mkArity (ctx,s)))
-    (number_of_inductives mib) in
-             (* Remark: all arities are closed hence no need for lift *)
-  let env_ar = push_rel_context (List.rev arities) env in
-  let uargs = List.map (lift (number_of_inductives mib)) uargs in
-  let lc =
-    Array.map (fun mip ->
-        Array.map (fun c -> 
-	    instantiate_partial_params c uargs mib.mind_params_ctxt)
-          mip.mind_nf_lc)
-      mib.mind_packets in
-  env_ar, lc, levels
-
-let is_small_inductive (mip,mib) = is_small (snd (destArity mib.mind_nf_arity))
-
-let max_inductive_sort v =
-  let v = Array.map (function
-    | Type u -> u
-    | _ -> anomaly "Only type levels when computing the minimal sort of an inductive type") v in
-  Univ.sup_array v
-
-(* Type of an inductive type *)
-
-let type_of_inductive (_,mip) = mip.mind_user_arity
+let sort_as_univ = function
+| Type u -> u
+| Prop Null -> neutral_univ
+| Prop Pos -> base_univ
+
+let rec make_subst env exp act =
+  match exp, act with
+  (* Bind expected levels of parameters to actual levels *)
+  | None :: exp, _ :: act ->
+      make_subst env exp act
+  | Some u :: exp, t :: act -> 
+      (u, sort_as_univ (snd (dest_arity env t))) :: make_subst env exp act
+  (* Not enough parameters, create a fresh univ *)
+  | Some u :: exp, [] ->
+      (u, fresh_local_univ ()) :: make_subst env exp []
+  | None :: exp, [] ->
+      make_subst env exp []
+  (* Uniform parameters are exhausted *)
+  | [], _ -> []
+
+let sort_of_instantiated_universe mip subst level =
+  let level = subst_large_constraints subst level in
+  let nci = number_of_constructors mip in
+  if nci = 0 then mk_Prop
+  else
+    if is_empty_univ level then if nci = 1 then mk_Prop else mk_Set 
+    else if is_base_univ level then mk_Set
+    else Type level
+
+let instantiate_inductive_with_param_levels env ar mip paramtyps =
+  let args = Array.to_list paramtyps in
+  let subst = make_subst env ar.mind_param_levels args in
+  sort_of_instantiated_universe mip subst ar.mind_level
+
+let type_of_inductive_knowing_parameters env mip paramtyps =
+  match mip.mind_arity with
+  | Monomorphic s ->
+      s.mind_user_arity
+  | Polymorphic ar ->
+      let s = instantiate_inductive_with_param_levels env ar mip paramtyps in
+      mkArity (mip.mind_arity_ctxt,s)
+
+(* The max of an array of universes *)
+
+let cumulate_constructor_univ u = function
+  | Prop Null -> u
+  | Prop Pos -> sup base_univ u
+  | Type u' -> sup u u'
+
+let max_inductive_sort =
+  Array.fold_left cumulate_constructor_univ neutral_univ
+
+(* Type of a (non applied) inductive type *)
+
+let type_of_inductive (_,mip) =
+  match mip.mind_arity with
+  | Monomorphic s -> s.mind_user_arity
+  | Polymorphic s ->
+      let subst = map_succeed (function
+	| Some u -> (u, fresh_local_univ ())
+	| None -> failwith "") s.mind_param_levels in
+      let s = mkSort (sort_of_instantiated_universe mip subst s.mind_level) in
+      it_mkProd_or_LetIn s mip.mind_arity_ctxt
 
 (************************************************************************)
 (* Type of a constructor *)
@@ -215,19 +216,11 @@ let arities_of_constructors ind specif =
 
 (************************************************************************)
 
-let is_info_arity env c =
-  match dest_arity env c with
-    | (_,Prop Null) -> false 
-    | (_,Prop Pos)  -> true 
-    | (_,Type _)    -> true
-
-let error_elim_expln env kp ki =
-  if is_info_arity env kp && not (is_info_arity env ki) then
-    NonInformativeToInformative
-  else 
-    match (kind_of_term kp,kind_of_term ki) with 
-      | Sort (Type _), Sort (Prop _) -> StrongEliminationOnNonSmallType
-      | _ -> WrongArity
+let error_elim_expln kp ki =
+  match kp,ki with
+  | (InType | InSet), InProp -> NonInformativeToInformative
+  | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
+  | _ -> WrongArity
 
 (* Type of case predicates *)
 
@@ -244,9 +237,20 @@ let local_rels ctxt =
   rels
 
 (* Get type of inductive, with parameters instantiated *)
-let get_arity mib mip params =
-  let arity = mip.mind_nf_arity in
-  destArity (full_inductive_instantiate mib params arity)
+
+let inductive_sort_family mip =
+  match mip.mind_arity with
+   | Monomorphic s -> family_of_sort s.mind_sort 
+   | Polymorphic _ -> InType
+
+let mind_arity mip =
+  mip.mind_arity_ctxt, inductive_sort_family mip
+
+let get_instantiated_arity (mib,mip) params =
+  let sign, s = mind_arity mip in
+  full_inductive_instantiate mib params sign, s
+
+let elim_sorts (_,mip) = mip.mind_kelim
 
 let rel_list n m = 
   let rec reln l p = 
@@ -254,66 +258,48 @@ let rel_list n m =
   in 
   reln [] 1
 
-let build_dependent_inductive ind mib mip params =
+let build_dependent_inductive ind (_,mip) params =
   let nrealargs = mip.mind_nrealargs in
   applist 
     (mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
 
-
 (* This exception is local *)
-exception LocalArity of (constr * constr * arity_error) option
+exception LocalArity of (sorts_family * sorts_family * arity_error) option
 
-let is_correct_arity env c pj ind mib mip params = 
-  let kelim = mip.mind_kelim in
-  let arsign,s = get_arity mib mip params in
-  let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in
-  let rec srec env pt t u =
+let check_allowed_sort ksort specif =
+  if not (List.exists ((=) ksort) (elim_sorts specif)) then 
+    let s = inductive_sort_family (snd specif) in
+    raise (LocalArity (Some(ksort,s,error_elim_expln ksort s)))
+
+let is_correct_arity env c pj ind specif params = 
+  let arsign,_ = get_instantiated_arity specif params in
+  let rec srec env pt ar u =
     let pt' = whd_betadeltaiota env pt in
-    let t' = whd_betadeltaiota env t in
-    match kind_of_term pt', kind_of_term t' with
-      | Prod (na1,a1,a2), Prod (_,a1',a2') ->
+    match kind_of_term pt', ar with
+      | Prod (na1,a1,t), (_,None,a1')::ar' ->
           let univ =
             try conv env a1 a1'
             with NotConvertible -> raise (LocalArity None) in
-          srec (push_rel (na1,None,a1) env) a2 a2' (Constraint.union u univ)
-      | Prod (_,a1,a2), _ -> 
-          let k = whd_betadeltaiota env a2 in 
-          let ksort = match kind_of_term k with
+          srec (push_rel (na1,None,a1) env) t ar' (Constraint.union u univ)
+      | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
+          let ksort = match kind_of_term (whd_betadeltaiota env a2) with
             | Sort s -> family_of_sort s 
 	    | _ -> raise (LocalArity None) in
-
-	  let dep_ind = build_dependent_inductive ind mib mip params
-	  in 
+	  let dep_ind = build_dependent_inductive ind specif params in 
           let univ =
             try conv env a1 dep_ind
             with NotConvertible -> raise (LocalArity None) in
-          if List.exists ((=) ksort) kelim then
-	    (true, Constraint.union u univ)
-          else 
-	    raise (LocalArity (Some(k,t',error_elim_expln env k t')))
-      | k, Prod (_,_,_) ->
+	  check_allowed_sort ksort specif;
+	  (true, Constraint.union u univ)
+      | Sort s', [] ->
+	  check_allowed_sort (family_of_sort s') specif;
+	  (false, u)
+      | _ ->
 	  raise (LocalArity None)
-      | k, ki -> 
-	  let ksort = match k with
-            | Sort s -> family_of_sort s 
-            | _ ->  raise (LocalArity None) in
-          if List.exists ((=) ksort) kelim then 
-	    (false, u)
-          else 
-	    raise (LocalArity (Some(pt',t',error_elim_expln env pt' t')))
   in 
-  try srec env pj.uj_type nodep_ar Constraint.empty
+  try srec env pj.uj_type (List.rev arsign) Constraint.empty
   with LocalArity kinds ->
-    let create_sort = function 
-      | InProp -> mkProp
-      | InSet -> mkSet
-      | InType -> mkSort type_0 in
-    let listarity = List.map create_sort kelim
-(*    let listarity =
-      (List.map (fun s -> make_arity env true indf (create_sort s)) kelim)
-      @(List.map (fun s -> make_arity env false indf (create_sort s)) kelim)*)
-    in 
-    error_elim_arity env ind listarity c pj kinds
+    error_elim_arity env ind (elim_sorts specif) c pj kinds
 
 
 (************************************************************************)
@@ -321,13 +307,13 @@ let is_correct_arity env c pj ind mib mip params =
 
 (* [p] is the predicate, [i] is the constructor number (starting from 0),
    and [cty] is the type of the constructor (params not instantiated) *)
-let build_branches_type ind mib mip params dep p =
+let build_branches_type ind (_,mip as specif) params dep p =
   let build_one_branch i cty =
-    let typi = full_constructor_instantiate ((ind,mib,mip),params) cty in
+    let typi = full_constructor_instantiate (ind,specif,params) cty in
     let (args,ccl) = decompose_prod_assum typi in
     let nargs = rel_context_length args in
     let (_,allargs) = decompose_app ccl in
-    let (lparams,vargs) = list_chop mib.mind_nparams allargs in
+    let (lparams,vargs) = list_chop (inductive_params specif) allargs in
     let cargs =
       if dep then
         let cstr = ith_constructor_of_inductive ind (i+1) in
@@ -346,12 +332,12 @@ let build_case_type dep p c realargs =
   beta_appvect p (Array.of_list args)
 
 let type_case_branches env (ind,largs) pj c =
-  let (mib,mip) = lookup_mind_specif env ind in 
-  let nparams = mib.mind_nparams in
+  let specif = lookup_mind_specif env ind in 
+  let nparams = inductive_params specif in
   let (params,realargs) = list_chop nparams largs in
   let p = pj.uj_val in
-  let (dep,univ) = is_correct_arity env c pj ind mib mip params in
-  let lc = build_branches_type ind mib mip params dep p in
+  let (dep,univ) = is_correct_arity env c pj ind specif params in
+  let lc = build_branches_type ind specif params dep p in
   let ty = build_case_type dep p c realargs in
   (lc, ty, univ)
 
@@ -399,24 +385,27 @@ let check_case_info env indsp ci =
    first argument.
 *)
 
-(*************************)
-(* Environment annotated with marks on recursive arguments:
-   it is a triple (env,lst,n) where
-   - env is the typing environment
-   - lst is a mapping from de Bruijn indices to list of recargs
-     (tells which subterms of that variable are recursive)
-   - n is the de Bruijn index of the fixpoint for which we are
-     checking the guard condition.
+(*************************************************************)
+(* Environment annotated with marks on recursive arguments *)
 
-   Below are functions to handle such environment.
- *)
+(* tells whether it is a strict or loose subterm *)
 type size = Large | Strict
 
+(* merging information *)
 let size_glb s1 s2 =
   match s1,s2 with
       Strict, Strict -> Strict
     | _ -> Large
 
+(* possible specifications for a term:
+   - Not_subterm: when the size of a term is not related to the
+     recursive argument of the fixpoint
+   - Subterm: when the term is a subterm of the recursive argument
+       the wf_paths argument specifies which subterms are recursive
+   - Dead_code: when the term has been built by elimination over an
+       empty type
+ *)
+
 type subterm_spec =
     Subterm of (size * wf_paths)
   | Dead_code
@@ -517,31 +506,14 @@ let lookup_subterms env ind =
 
 (*********************************)
 
-(* finds the inductive type of the recursive argument of a fixpoint *)
-let inductive_of_fix env recarg body =
-  let (ctxt,b) = decompose_lam_n_assum recarg body in
-  let env' = push_rel_context ctxt env in
-  let (_,ty,_) = destLambda(whd_betadeltaiota env' b) in
-  let (i,_) = decompose_app (whd_betadeltaiota env' ty) in 
-  destInd i
-
-(* 
-   subterm_specif env c ind 
-
-   subterm_specif should test if [c] (building objects of inductive
-   type [ind], not necessarily the same as that of the recursive
-   argument) is a subterm of the recursive argument of the fixpoint we
-   are checking and fails with Not_found if not. In case it is, it
-   should send its recursive specification (i.e. on which arguments we
-   are allowed to make recursive calls). This recursive spec should be
-   the same size as the number of constructors of the type of c.
-
-   Returns:
-   - [Some lc] if [c] is a strict subterm of the rec. arg. (or a Meta) 
-   - [None] otherwise
+(* [subterm_specif renv t] computes the recursive structure of [t] and
+   compare its size with the size of the initial recursive argument of
+   the fixpoint we are checking. [renv] collects such information
+   about variables.
 *)
 
-let rec subterm_specif renv t ind = 
+let rec subterm_specif renv t = 
+  (* maybe reduction is not always necessary! *)
   let f,l = decompose_app (whd_betadeltaiota renv.env t) in
   match kind_of_term f with 
     | Rel k -> subterm_var k renv
@@ -551,7 +523,7 @@ let rec subterm_specif renv t ind =
         else
           let lbr_spec = case_branches_specif renv c ci.ci_ind lbr in
           let stl  =
-            Array.map (fun (renv',br') -> subterm_specif renv' br' ind)
+            Array.map (fun (renv',br') -> subterm_specif renv' br')
               lbr_spec in
           subterm_spec_glb stl
 	       
@@ -561,33 +533,43 @@ let rec subterm_specif renv t ind =
    furthermore when f is applied to a term which is strictly less than
    n, one may assume that x itself is strictly less than n
 *)
-        let nbfix = Array.length typarray in
-        let recargs = lookup_subterms renv.env ind in
-        (* pushing the fixpoints *)
-        let renv' = push_fix_renv renv recdef in
-        let renv' =
-          assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
-        let decrArg = recindxs.(i) in 
-        let theBody = bodies.(i)   in
-        let nbOfAbst = decrArg+1 in
-        let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
-        (* pushing the fix parameters *)
-        let renv'' = push_ctxt_renv renv' sign in
-        let renv'' =
-          if List.length l < nbOfAbst then renv''
-          else
-            let decrarg_ind = inductive_of_fix renv''.env decrArg theBody in
-            let theDecrArg  = List.nth l decrArg in
-	    let arg_spec    = subterm_specif renv theDecrArg decrarg_ind in
-            assign_var_spec renv'' (1, arg_spec) in
-	subterm_specif renv'' strippedBody ind
-	    
+        let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
+        let oind =
+          let env' = push_rel_context ctxt renv.env in
+          try Some(fst(find_inductive env' clfix))
+          with Not_found -> None in
+        (match oind with
+            None -> Not_subterm (* happens if fix is polymorphic *)
+          | Some ind ->
+              let nbfix = Array.length typarray in
+              let recargs = lookup_subterms renv.env ind in
+              (* pushing the fixpoints *)
+              let renv' = push_fix_renv renv recdef in
+              let renv' =
+                (* Why Strict here ? To be general, it could also be
+                   Large... *)
+                assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
+              let decrArg = recindxs.(i) in 
+              let theBody = bodies.(i)   in
+              let nbOfAbst = decrArg+1 in
+              let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
+              (* pushing the fix parameters *)
+              let renv'' = push_ctxt_renv renv' sign in
+              let renv'' =
+                if List.length l < nbOfAbst then renv''
+                else
+                  let theDecrArg  = List.nth l decrArg in
+	          let arg_spec    = subterm_specif renv theDecrArg in
+                  assign_var_spec renv'' (1, arg_spec) in
+	      subterm_specif renv'' strippedBody)
+
     | Lambda (x,a,b) -> 
         assert (l=[]);
-        subterm_specif (push_var_renv renv (x,a)) b ind
+        subterm_specif (push_var_renv renv (x,a)) b
+
+    (* Metas and evars are considered OK *)
+    | (Meta _|Evar _) -> Dead_code
 
-    (* A term with metas is considered OK *)
-    | Meta _ -> Dead_code
     (* Other terms are not subterms *)
     | _ -> Not_subterm
 
@@ -595,16 +577,20 @@ let rec subterm_specif renv t ind =
    object is a recursive subterm then compute the information
    associated to its own subterms.
    Rq: if branch is not eta-long, then the recursive information
-   is not propagated *)
+   is not propagated to the missing abstractions *)
 and case_branches_specif renv c ind lbr = 
-  let c_spec = subterm_specif renv c ind in
+  let c_spec = subterm_specif renv c in
   let rec push_branch_args renv lrec c = 
-    let c' = strip_outer_cast (whd_betadeltaiota renv.env c) in 
-    match lrec, kind_of_term c' with 
-      |	(ra::lr,Lambda (x,a,b)) ->
-          let renv' = push_var renv (x,a,ra) in
-          push_branch_args renv' lr b
-      | (_,_) -> (renv,c') in
+    match lrec with
+        ra::lr ->
+          let c' = whd_betadeltaiota renv.env c in
+          (match kind_of_term c' with
+              Lambda(x,a,b) ->
+                let renv' = push_var renv (x,a,ra) in
+                push_branch_args renv' lr b
+            | _ -> (* branch not in eta-long form: cannot perform rec. calls *)
+                (renv,c'))
+      | [] -> (renv, c) in
   match c_spec with
       Subterm (_,t) ->
         let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
@@ -618,8 +604,8 @@ and case_branches_specif renv c ind lbr =
     | Not_subterm -> Array.map (fun c -> (renv,c)) lbr
 
 (* Check term c can be applied to one of the mutual fixpoints. *)
-let check_is_subterm renv c ind = 
-  match subterm_specif renv c ind with
+let check_is_subterm renv c = 
+  match subterm_specif renv c with
     Subterm (Strict,_) | Dead_code -> true
   |  _ -> false
 
@@ -642,42 +628,45 @@ let error_illegal_rec_call renv fx arg =
 let error_partial_apply renv fx =
   raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
 
-
 (* Check if [def] is a guarded fixpoint body with decreasing arg.
    given [recpos], the decreasing arguments of each mutually defined
    fixpoint. *)
 let check_one_fix renv recpos def =
   let nfi = Array.length recpos in 
+
+  (* Checks if [t] only make valid recursive calls *)
   let rec check_rec_call renv t = 
     (* if [t] does not make recursive calls, it is guarded: *)
-    noccur_with_meta renv.rel_min nfi t or 
-    (* Rq: why not try and expand some definitions ? *)
-    let f,l = decompose_app (whd_betaiotazeta renv.env t) in
-    match kind_of_term f with
-      | Rel p -> 
-          (* Test if it is a recursive call: *) 
-	  if renv.rel_min <= p & p < renv.rel_min+nfi then
-            (* the position of the invoked fixpoint: *) 
-	    let glob = renv.rel_min+nfi-1-p in
-            (* the decreasing arg of the rec call: *)
-	    let np = recpos.(glob) in
-            if List.length l <= np then error_partial_apply renv glob;
-	    match list_chop np l with
-		(la,(z::lrest)) -> 
-                  (* Check the decreasing arg is smaller *)
-	          if not (check_is_subterm renv z renv.inds.(glob)) then
-                    error_illegal_rec_call renv glob z;
-                  List.for_all (check_rec_call renv) (la@lrest)
-		| _ -> assert false
-          (* otherwise check the arguments are guarded: *)
-	  else List.for_all (check_rec_call renv) l        
+    if noccur_with_meta renv.rel_min nfi t then ()
+    else
+      (* Rq: why not try and expand some definitions ? *)
+      let f,l = decompose_app (whd_betaiotazeta renv.env t) in
+      match kind_of_term f with
+        | Rel p -> 
+            (* Test if [p] is a fixpoint (recursive call) *) 
+	    if renv.rel_min <= p & p < renv.rel_min+nfi then
+              (* the position of the invoked fixpoint: *) 
+	      let glob = renv.rel_min+nfi-1-p in
+              (* the decreasing arg of the rec call: *)
+	      let np = recpos.(glob) in
+              if List.length l <= np then error_partial_apply renv glob
+              else
+	        (match list_chop np l with
+		    (la,(z::lrest)) -> 
+                      (* Check the decreasing arg is smaller *)
+	              if not (check_is_subterm renv z) then
+                        error_illegal_rec_call renv glob z;
+                      List.iter (check_rec_call renv) (la@lrest)
+	          | _ -> assert false)
+            (* otherwise check the arguments are guarded: *)
+	    else List.iter (check_rec_call renv) l        
 
       | Case (ci,p,c_0,lrest) ->
-          List.for_all (check_rec_call renv) (c_0::p::l) &&
+          List.iter (check_rec_call renv) (c_0::p::l);
           (* compute the recarg information for the arguments of
              each branch *)
           let lbr = case_branches_specif renv c_0 ci.ci_ind lrest in
-          array_for_all (fun (renv',br') -> check_rec_call renv' br') lbr
+          Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
 
   (* Enables to traverse Fixpoint definitions in a more intelligent
      way, ie, the rule :
@@ -695,65 +684,58 @@ let check_one_fix renv recpos def =
      Eduardo 7/9/98 *)
 
       | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
-          List.for_all (check_rec_call renv) l &&
-          array_for_all (check_rec_call renv) typarray && 
+          List.iter (check_rec_call renv) l;
+          Array.iter (check_rec_call renv) typarray;
           let decrArg = recindxs.(i) in
           let renv' = push_fix_renv renv recdef in 
           if (List.length l < (decrArg+1)) then
-	    array_for_all (check_rec_call renv') bodies
+	    Array.iter (check_rec_call renv') bodies
           else 
-            let ok_vect =
-              Array.mapi
-                (fun j body ->
-                  if i=j then
-                    let decrarg_ind =
-                      inductive_of_fix renv'.env decrArg body in
-                    let theDecrArg  = List.nth l decrArg in
-	            let arg_spec =
-                      subterm_specif renv theDecrArg decrarg_ind in
-	            check_nested_fix_body renv' (decrArg+1) arg_spec body
-                  else check_rec_call renv' body)
-                bodies in
-            array_for_all (fun b -> b) ok_vect
+            Array.iteri
+              (fun j body ->
+                if i=j then
+                  let theDecrArg  = List.nth l decrArg in
+	          let arg_spec = subterm_specif renv theDecrArg in
+	          check_nested_fix_body renv' (decrArg+1) arg_spec body
+                else check_rec_call renv' body)
+              bodies
 
       | Const kn -> 
-          (try List.for_all (check_rec_call renv) l
-           with (FixGuardError _ ) as e ->
-             if evaluable_constant kn renv.env then 
-	       check_rec_call renv
-                 (applist(constant_value renv.env kn, l))
-	     else raise e)
+          if evaluable_constant kn renv.env then 
+            try List.iter (check_rec_call renv) l
+            with (FixGuardError _ ) ->
+	      check_rec_call renv(applist(constant_value renv.env kn, l))
+	  else List.iter (check_rec_call renv) l
 
       (* The cases below simply check recursively the condition on the
          subterms *)
       | Cast (a,_, b) -> 
-          List.for_all (check_rec_call renv) (a::b::l)
+          List.iter (check_rec_call renv) (a::b::l)
 
       | Lambda (x,a,b) ->
-          check_rec_call (push_var_renv renv (x,a)) b &&
-          List.for_all (check_rec_call renv) (a::l)
+          check_rec_call (push_var_renv renv (x,a)) b;
+          List.iter (check_rec_call renv) (a::l)
 
       | Prod (x,a,b) -> 
-          check_rec_call (push_var_renv renv (x,a)) b &&
-          List.for_all (check_rec_call renv) (a::l)
+          check_rec_call (push_var_renv renv (x,a)) b;
+          List.iter (check_rec_call renv) (a::l)
 
       | CoFix (i,(_,typarray,bodies as recdef)) ->
-	  array_for_all (check_rec_call renv) typarray &&
-          List.for_all (check_rec_call renv) l &&
+	  Array.iter (check_rec_call renv) typarray;
+          List.iter (check_rec_call renv) l;
 	  let renv' = push_fix_renv renv recdef in
-	  array_for_all (check_rec_call renv') bodies
-
-      | Evar (_,la) -> 
-	  array_for_all (check_rec_call renv) la &&
-          List.for_all (check_rec_call renv) l
+	  Array.iter (check_rec_call renv') bodies
 
-      | Meta _ -> true
+      | Evar _ -> 
+          List.iter (check_rec_call renv) l
 
-      | (App _ | LetIn _) -> 
-	  anomaly "check_rec_call: should have been reduced"
+      (* l is not checked because it is considered as the meta's context *)
+      | Meta _ -> ()
 
       | (Ind _ | Construct _ | Var _ | Sort _) ->
-          List.for_all (check_rec_call renv) l
+          List.iter (check_rec_call renv) l
+
+      | (App _ | LetIn _) -> assert false (* beta zeta reduction *)
 
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if decr = 0 then
@@ -761,11 +743,11 @@ let check_one_fix renv recpos def =
     else
       match kind_of_term body with
 	| Lambda (x,a,b) ->
+	    check_rec_call renv a;
             let renv' = push_var_renv renv (x,a) in
-	    check_rec_call renv a &&
 	    check_nested_fix_body renv' (decr-1) recArgsDecrArg b
 	| _ -> anomaly "Not enough abstractions in fix body"
-    
+
   in
   check_rec_call renv def
 
@@ -784,7 +766,6 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     error_ill_formed_rec_body env err names i in
   (* Check the i-th definition with recarg k *)
   let find_ind i k def = 
-    if k < 0 then anomaly "negative recarg position";
     (* check fi does not appear in the k+1 first abstractions, 
        gives the type of the k+1-eme abstraction (must be an inductive)  *)
     let rec check_occur env n def = 
@@ -813,8 +794,7 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) =
   for i = 0 to Array.length bodies - 1 do
     let (fenv,body) = rdef.(i) in
     let renv = make_renv fenv minds nvect.(i) minds.(i) in
-    try
-      let _ = check_one_fix renv nvect body in ()
+    try check_one_fix renv nvect body
     with FixGuardError (fixenv,err) ->
       error_ill_formed_rec_body fixenv err names i
   done
@@ -825,14 +805,6 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
 *)
 
 (************************************************************************)
-(* Scrape *)
-
-let rec scrape_mind env kn = 
-  match (Environ.lookup_mind kn env).mind_equiv with
-    | None -> kn
-    | Some kn' -> scrape_mind env kn'
-
-(************************************************************************)
 (* Co-fixpoints. *)
 
 exception CoFixGuardError of env * guard_error
@@ -852,25 +824,19 @@ let rec codomain_is_coind env c =
 
 let check_one_cofix env nbfix def deftype = 
   let rec check_rec_call env alreadygrd n vlra  t =
-    if noccur_with_meta n nbfix t then
-      true 
-    else
+    if not (noccur_with_meta n nbfix t) then
       let c,args = decompose_app (whd_betadeltaiota env t) in
       match kind_of_term c with 
-	| Meta _ -> true
-	      
 	| Rel p when  n <= p && p < n+nbfix ->
-	    (* recursive call *)
-            if alreadygrd then
-	      if List.for_all (noccur_with_meta n nbfix) args then
-		true
-	      else 
-		raise (CoFixGuardError (env,NestedRecursiveOccurrences))
-            else 
+	    (* recursive call: must be guarded and no nested recursive
+               call allowed *)
+            if not alreadygrd then
 	      raise (CoFixGuardError (env,UnguardedRecursiveCall t))
+            else if not(List.for_all (noccur_with_meta n nbfix) args) then
+	      raise (CoFixGuardError (env,NestedRecursiveOccurrences))
 		 
 	| Construct (_,i as cstr_kn)  ->
-            let lra =vlra.(i-1) in 
+            let lra = vlra.(i-1) in 
             let mI = inductive_of_constructor cstr_kn in
 	    let (mib,mip) = lookup_mind_specif env mI in
             let realargs = list_skipn mib.mind_nparams args in
@@ -883,17 +849,17 @@ let check_one_cofix env nbfix def deftype =
 		                 (env,RecCallInNonRecArgOfConstructor t))
                   else
                     let spec = dest_subterms rar in
-                    check_rec_call env true n spec t &&
+                    check_rec_call env true n spec t;
                     process_args_of_constr (lr, lrar)
-              | [],_ -> true 
+              | [],_ -> ()
               | _ -> anomaly_ill_typed () 
             in process_args_of_constr (realargs, lra)
 		 
 	| Lambda (x,a,b) ->
 	     assert (args = []);
-            if (noccur_with_meta n nbfix a) then
-              check_rec_call (push_rel (x, None, a) env)
-		alreadygrd (n+1)  vlra b
+            if noccur_with_meta n nbfix a then
+              let env' = push_rel (x, None, a) env in
+              check_rec_call env' alreadygrd (n+1)  vlra b
             else 
 	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
 	      
@@ -903,10 +869,8 @@ let check_one_cofix env nbfix def deftype =
               let nbfix = Array.length vdefs in
 	      if (array_for_all (noccur_with_meta n nbfix) varit) then
 		let env' = push_rec_types recdef env in
-		(array_for_all
-		   (check_rec_call env' alreadygrd (n+1) vlra) vdefs)
-		&&
-		(List.for_all (check_rec_call env alreadygrd (n+1) vlra) args) 
+		(Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs;
+		 List.iter (check_rec_call env alreadygrd n vlra) args)
               else 
 		raise (CoFixGuardError (env,RecCallInTypeOfDef c))
 	    else
@@ -916,7 +880,7 @@ let check_one_cofix env nbfix def deftype =
             if (noccur_with_meta n nbfix p) then
               if (noccur_with_meta n nbfix tm) then
 		if (List.for_all (noccur_with_meta n nbfix) args) then
-		  (array_for_all (check_rec_call env alreadygrd n vlra) vrest)
+		  Array.iter (check_rec_call env alreadygrd n vlra) vrest
 		else 
 		  raise (CoFixGuardError (env,RecCallInCaseFun c))
               else 
@@ -924,7 +888,12 @@ let check_one_cofix env nbfix def deftype =
             else 
 	      raise (CoFixGuardError (env,RecCallInCasePred c))
               
+	| Meta _ -> ()
+        | Evar _ ->
+	    List.iter (check_rec_call env alreadygrd n vlra) args
+	      
 	| _    -> raise (CoFixGuardError (env,NotGuardedForm t)) in 
+
   let (mind, _) = codomain_is_coind env deftype in
   let vlra = lookup_subterms env mind in
   check_rec_call env false 1 (dest_subterms vlra) def
@@ -936,9 +905,7 @@ let check_cofix env (bodynum,(names,types,bodies as recdef)) =
   let nbfix = Array.length bodies in 
   for i = 0 to nbfix-1 do
     let fixenv = push_rec_types recdef env in
-    try 
-      let _ = check_one_cofix fixenv nbfix bodies.(i) types.(i)
-      in ()
+    try check_one_cofix fixenv nbfix bodies.(i) types.(i)
     with CoFixGuardError (errenv,err) -> 
       error_ill_formed_rec_body errenv err names i
   done