Applicative commutative cuts in Fixpoint guard condition

In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm
property of "u" in the analysis of "t".

Commutative cuts aren't compatible with typing so we need to ensure that
term of "x"'s type and term of "u"'s have the same subterm_spec.
Consequently,declaration.MRec argument has changed to the inductive name
instead of only the number of the inductive in the mutual_inductive
family.

In subterm_specif and check_rec_call, arguments are stored in a stack.
At each lambda, one element is popped to add in renv a smarter
subterm_spec for the variable. subterm_spec of constructor's argument
was added this way, the job is now done more often.

Some eta contracted match branches are now accepted but enforcing
eta-expansion of branches might be anyway a recommended invariant.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 196 insertions, 201 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 4f98bb8b0..c7f808742 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -71,7 +71,7 @@ let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
 
 type recarg =
   | Norec
-  | Mrec of int
+  | Mrec of inductive
   | Imbr of inductive
 
 let subst_recarg sub r = match r with
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 15c5350b0..3e8de34c4 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -51,7 +51,7 @@ val subst_const_body : substitution -> constant_body -> constant_body
 
 type recarg =
   | Norec
-  | Mrec of int
+  | Mrec of inductive
   | Imbr of inductive
 
 val subst_recarg : substitution -> recarg -> recarg
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a9f8fa7c6..c3d79ee4a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -402,7 +402,7 @@ let array_min nmr a = if nmr = 0 then 0 else
 
 (* The recursive function that checks positivity and builds the list
    of recursive arguments *)
-let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
+let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
   let lparams = rel_context_length hyps in
   let nmr = rel_context_nhyps hyps in
   (* Checking the (strict) positivity of a constructor argument type [c] *)
@@ -446,6 +446,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
       with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
       (* If the inductive appears in the args (non params) then the
 	 definition is not positive. *)
+
       if not (List.for_all (noccur_between n ntypes) auxlargs) then
 	failwith_non_pos_list n ntypes auxlargs;
       (* We do not deal with imbricated mutual inductive types *)
@@ -511,11 +512,11 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
   in
   let irecargs = Array.map snd irecargs_nmr
   and nmr' = array_min nmr irecargs_nmr
-  in (nmr', mk_paths (Mrec i) irecargs)
+  in (nmr', mk_paths (Mrec ind) irecargs)
 
-let check_positivity env_ar params inds =
+let check_positivity kn env_ar params inds =
   let ntypes = Array.length inds in
-  let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in
+  let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = List.rev (Array.to_list rc) in
   let lparams = rel_context_length params in
   let nmr = rel_context_nhyps params in
@@ -524,7 +525,7 @@ let check_positivity env_ar params inds =
       list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
     let nargs = rel_context_nhyps sign - nmr in
-    check_positivity_one ienv params i nargs lcnames lc
+    check_positivity_one ienv params (kn,i) nargs lcnames lc
   in
   let irecargs_nmr = Array.mapi check_one inds in
   let irecargs = Array.map snd irecargs_nmr
@@ -655,11 +656,11 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 (************************************************************************)
 (************************************************************************)
 
-let check_inductive env mie =
+let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar, params, inds, cst) = typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let (nmr,recargs) = check_positivity env_ar params inds in
+  let (nmr,recargs) = check_positivity kn env_ar params inds in
   (* Build the inductive packets *)
     build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite
       inds nmr recargs cst
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index a3867c6b8..40d6912c4 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -37,4 +37,4 @@ exception InductiveError of inductive_error
 (** The following function does checks on inductive declarations. *)
 
 val check_inductive :
-  env -> mutual_inductive_entry -> mutual_inductive_body
+  env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9215ac0c6..f3f0e2217 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -438,27 +438,20 @@ type guard_env =
   { env     : env;
     (* dB of last fixpoint *)
     rel_min : int;
-    (* inductive of recarg of each fixpoint *)
-    inds    : inductive array;
-    (* the recarg information of inductive family *)
-    recvec  : wf_paths array;
     (* dB of variables denoting subterms *)
     genv    : subterm_spec Lazy.t list;
   }
 
-let make_renv env minds recarg (kn,tyi) =
+let make_renv env recarg (kn,tyi) =
   let mib = Environ.lookup_mind kn env in
   let mind_recvec =
     Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
   { env = env;
     rel_min = recarg+2;
-    inds = minds;
-    recvec = mind_recvec;
     genv = [Lazy.lazy_from_val(Subterm(Large,mind_recvec.(tyi)))] }
 
 let push_var renv (x,ty,spec) =
-  { renv with
-    env = push_rel (x,None,ty) renv.env;
+  { env = push_rel (x,None,ty) renv.env;
     rel_min = renv.rel_min+1;
     genv = spec:: renv.genv }
 
@@ -473,69 +466,43 @@ let subterm_var p renv =
   try Lazy.force (List.nth renv.genv (p-1))
   with Failure _ | Invalid_argument _ -> Not_subterm
 
-(* Add a variable and mark it as strictly smaller with information [spec]. *)
-let add_subterm renv (x,a,spec) =
-  push_var renv (x,a,spec_of_tree spec)
-
 let push_ctxt_renv renv ctxt =
   let n = rel_context_length ctxt in
-  { renv with
-    env = push_rel_context ctxt renv.env;
+  { env = push_rel_context ctxt renv.env;
     rel_min = renv.rel_min+n;
     genv = iterate (fun ge -> lazy Not_subterm::ge) n renv.genv }
 
 let push_fix_renv renv (_,v,_ as recdef) =
   let n = Array.length v in
-  { renv with
-    env = push_rec_types recdef renv.env;
+  { env = push_rec_types recdef renv.env;
     rel_min = renv.rel_min+n;
     genv = iterate (fun ge -> lazy Not_subterm::ge) n renv.genv }
 
+(* Definition and manipulation of the stack *)
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
 
-(******************************)
-(* Computing the recursive subterms of a term (propagation of size
-   information through Cases). *)
+let push_stack_closures renv l stack = 
+  List.fold_right (fun h b -> (SClosure (renv,h))::b) l stack
 
-(*
-   c is a branch of an inductive definition corresponding to the spec
-   lrec.  mind_recvec is the recursive spec of the inductive
-   definition of the decreasing argument n.
-
-   case_branches_specif renv lrec lc will pass the lambdas
-   of c corresponding to pattern variables and collect possibly new
-   subterms variables and returns the bodies of the branches with the
-   correct envs and decreasing args.
-*)
+let push_stack_args l stack = 
+  List.fold_right (fun h b -> (SArg h)::b) l stack
+
+(******************************)
+(* {6 Computing the recursive subterms of a term (propagation of size
+   information through Cases).} *)
 
 let lookup_subterms env ind =
   let (_,mip) = lookup_mind_specif env ind in
   mip.mind_recargs
 
-(*********************************)
-
-(* Propagation of size information through Cases: if the matched
-   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 to the missing abstractions *)
-let case_branches_specif renv c_spec ci lbr =
-  let car =
+(* In {match c as z in ci y_s return P with |C_i x_s => t end}
+   [branches_specif renv c_spec ci] returns an array of x_s specs knowing
+   c_spec. *)
+let branches_specif renv c_spec ci =
+  let car = 
     let (_,mip) = lookup_mind_specif renv.env ci.ci_ind in
     let v = dest_subterms mip.mind_recargs in
-    Array.map List.length v in
-  let rec push_branch_args renv lrec c =
-    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
-
-  let sub_spec =
+      Array.map List.length v in
     Array.mapi
       (fun i nca -> (* i+1-th cstructor has arity nca *)
 	 let cs = lazy 
@@ -546,9 +513,7 @@ let case_branches_specif renv c_spec ci lbr =
 	      | Dead_code -> Array.create nca (lazy Dead_code)
 	      | Not_subterm -> Array.create nca (lazy Not_subterm)) in
 	 list_tabulate (fun j -> (Lazy.force cs).(j)) nca)
-      car in
-  assert (Array.length sub_spec = Array.length lbr);
-  array_map2 (push_branch_args renv) sub_spec lbr
+      car 
 
 (* [subterm_specif renv t] computes the recursive structure of [t] and
    compare its size with the size of the initial recursive argument of
@@ -556,78 +521,98 @@ let case_branches_specif renv c_spec ci lbr =
    about variables.
 *)
 
-let rec subterm_specif renv t =
+let rec subterm_specif renv stack 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
-
-    | Case (ci,_,c,lbr) ->
-        let lbr_spec = case_subterm_specif renv ci c lbr in
-        let stl  =
-          Array.map (fun (renv',br') -> subterm_specif renv' br')
-            lbr_spec in
-        subterm_spec_glb stl
-
-    | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
-(* when proving that the fixpoint f(x)=e is less than n, it is enough
-   to prove that e is less than n assuming f is less than n
-   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 (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, lazy (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    = lazy_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
-
-    (* Metas and evars are considered OK *)
-    | (Meta _|Evar _) -> Dead_code
-
-    (* Other terms are not subterms *)
-    | _ -> Not_subterm
-
-and lazy_subterm_specif renv t =
-  lazy (subterm_specif renv t)
-
-and case_subterm_specif renv ci c lbr =
-  if Array.length lbr = 0 then [||]
-  else
-    let c_spec = lazy_subterm_specif renv c in
-    case_branches_specif renv c_spec ci lbr
- 
+    match kind_of_term f with
+      | Rel k -> subterm_var k renv
+
+      | Case (ci,_,c,lbr) ->
+	  let stack' = push_stack_closures renv l stack in
+          let cases_spec = branches_specif renv 
+	    (lazy_subterm_specif renv [] c) ci in
+          let stl  =
+            Array.mapi (fun i br' ->
+			  let stack_br = push_stack_args (cases_spec.(i)) stack' in
+			    subterm_specif renv stack_br br')
+              lbr in
+            subterm_spec_glb stl
+
+      | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
+	  (* when proving that the fixpoint f(x)=e is less than n, it is enough
+	     to prove that e is less than n assuming f is less than n
+	     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 (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, lazy (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 stack' = push_stack_closures renv l stack in
+		   let renv'' = push_ctxt_renv renv' sign in
+		   let renv'' =
+                     if List.length stack' < nbOfAbst then renv''
+                     else
+		       let decrArg = List.nth stack' decrArg in
+                       let arg_spec = stack_element_specif decrArg in
+			 assign_var_spec renv'' (1, arg_spec) in
+		     subterm_specif renv'' [] strippedBody)
+
+      | Lambda (x,a,b) ->
+          assert (l=[]);
+	  let spec,stack' = extract_stack renv a stack in
+	    subterm_specif (push_var renv (x,a,spec)) stack' b
+
+      (* Metas and evars are considered OK *)
+      | (Meta _|Evar _) -> Dead_code
+
+      (* Other terms are not subterms *)
+      | _ -> Not_subterm
+
+and lazy_subterm_specif renv stack t =
+  lazy (subterm_specif renv stack t)
+
+and stack_element_specif = function
+  |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h
+  |SArg x -> x
+
+and extract_stack renv a = function
+  |[] -> Lazy.lazy_from_val Not_subterm , []
+  |h::t -> lazy ((* because commutavive cuts are not compatible with typing, 
+		     arg_spec must carry the good wf_path *)
+       match Lazy.force (stack_element_specif h) with
+	     |Subterm(k,wpath) as spec -> begin
+	     	 try let (inda,_) = find_inductive renv.env a in
+	     	   match fst (Rtree.dest_node wpath) with
+		     |Norec -> assert false
+		     |(Mrec ind | Imbr ind) -> if inda = ind then spec else Dead_code
+	     	 with |Not_found -> Dead_code
+	     	   (* Something not of inductive type cannot be used as
+	     	      fixpoint recursive argument *)
+	       end
+	     |_ as spec -> spec) , t
+
 (* Check term c can be applied to one of the mutual fixpoints. *)
-let check_is_subterm renv c =
-  match subterm_specif renv c with
+let check_is_subterm x =
+  match Lazy.force x with
     Subterm (Strict,_) | Dead_code -> true
   |  _ -> false
 
@@ -635,7 +620,7 @@ let check_is_subterm renv c =
 
 exception FixGuardError of env * guard_error
 
-let error_illegal_rec_call renv fx arg =
+let error_illegal_rec_call renv fx (arg_renv,arg) =
   let (_,le_vars,lt_vars) =
     List.fold_left
       (fun (i,le,lt) sbt ->
@@ -645,7 +630,8 @@ let error_illegal_rec_call renv fx arg =
           | _ -> (i+1, le ,lt))
       (1,[],[]) renv.genv in
   raise (FixGuardError (renv.env,
-                        RecursionOnIllegalTerm(fx,arg,le_vars,lt_vars)))
+                        RecursionOnIllegalTerm(fx,(arg_renv.env, arg),
+					       le_vars,lt_vars)))
 
 let error_partial_apply renv fx =
   raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
@@ -656,8 +642,11 @@ let error_partial_apply renv fx =
 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 =
+  (* Checks if [t] only make valid recursive calls 
+     [stack] is the list of constructor's argument specification and 
+     arguments than will be applied after reduction.
+     example u in t where we have (match .. with |.. => t end) u *)
+  let rec check_rec_call renv stack t =
     (* if [t] does not make recursive calls, it is guarded: *)
     if noccur_with_meta renv.rel_min nfi t then ()
     else
@@ -667,35 +656,43 @@ let check_one_fix renv recpos def =
             (* Test if [p] is a fixpoint (recursive call) *)
 	    if renv.rel_min <= p & p < renv.rel_min+nfi then
               begin
-                List.iter (check_rec_call renv) l;
+                List.iter (check_rec_call renv []) l;
                 (* 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
+		let stack' = push_stack_closures renv l stack in
+                if List.length stack' <= np then error_partial_apply renv glob
                 else
                   (* Check the decreasing arg is smaller *)
-                  let z = List.nth l np in
-	          if not (check_is_subterm renv z) then
-                    error_illegal_rec_call renv glob z
+                  let z = List.nth stack' np in
+	          if not (check_is_subterm (stack_element_specif z)) then
+                    begin match z with
+		      |SClosure (z,z') -> error_illegal_rec_call renv glob (z,z') 
+		      |SArg _ -> error_partial_apply renv glob
+		    end
               end
             else
               begin
                 match pi2 (lookup_rel p renv.env) with
                 | None ->
-                    List.iter (check_rec_call renv) l
+                    List.iter (check_rec_call renv []) l
                 | Some c ->
-                    try List.iter (check_rec_call renv) l
+                    try List.iter (check_rec_call renv []) l
                     with FixGuardError _ ->
-                      check_rec_call renv (applist(lift p c,l))
+                      check_rec_call renv stack (applist(lift p c,l))
               end
-
+		
         | Case (ci,p,c_0,lrest) ->
-            List.iter (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_subterm_specif renv ci c_0 lrest in
-            Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
+            let case_spec = branches_specif renv 
+	      (lazy_subterm_specif renv [] c_0) ci in
+	    let stack' = push_stack_closures renv l stack in
+              Array.iteri (fun k br' -> 
+			     let stack_br = push_stack_args case_spec.(k) stack' in
+			     check_rec_call renv stack_br br') lrest
 
         (* Enables to traverse Fixpoint definitions in a more intelligent
            way, ie, the rule :
@@ -710,79 +707,79 @@ let check_one_fix renv recpos def =
            then f is guarded with respect to S in (g a1 ... am).
            Eduardo 7/9/98 *)
         | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
-            List.iter (check_rec_call renv) l;
-            Array.iter (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.iter (check_rec_call renv') bodies
-            else
+	    let stack' = push_stack_closures renv l stack in
               Array.iteri
                 (fun j body ->
-                  if i=j then
-                    let theDecrArg  = List.nth l decrArg in
-	            let arg_spec = lazy_subterm_specif renv theDecrArg in
-	            check_nested_fix_body renv' (decrArg+1) arg_spec body
-                  else check_rec_call renv' body)
+                   if i=j && (List.length stack' > decrArg) then
+		     let recArg = List.nth stack' decrArg in
+	             let arg_sp = stack_element_specif recArg in
+	             check_nested_fix_body renv' (decrArg+1) arg_sp body
+                   else check_rec_call renv' [] body)
                 bodies
 
         | Const kn ->
             if evaluable_constant kn renv.env then
-              try List.iter (check_rec_call renv) l
+              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.iter (check_rec_call renv) (a::b::l)
+		let value = (applist(constant_value renv.env kn, l)) in
+	        check_rec_call renv stack value
+	    else List.iter (check_rec_call renv []) l
 
         | Lambda (x,a,b) ->
-            List.iter (check_rec_call renv) (a::l);
-            check_rec_call (push_var_renv renv (x,a)) b
+	    assert (l = []);
+	    check_rec_call renv [] a ;
+	    let spec, stack' = extract_stack renv a stack in
+		     check_rec_call (push_var renv (x,a,spec)) stack' b
 
         | Prod (x,a,b) ->
-            List.iter (check_rec_call renv) (a::l);
-            check_rec_call (push_var_renv renv (x,a)) b
+	    assert (l = [] && stack = []);
+            check_rec_call renv [] a;
+            check_rec_call (push_var_renv renv (x,a)) [] b
 
         | CoFix (i,(_,typarray,bodies as recdef)) ->
-            List.iter (check_rec_call renv) l;
-	    Array.iter (check_rec_call renv) typarray;
+            List.iter (check_rec_call renv []) l;
+	    Array.iter (check_rec_call renv []) typarray;
 	    let renv' = push_fix_renv renv recdef in
-	    Array.iter (check_rec_call renv') bodies
+	    Array.iter (check_rec_call renv' []) bodies
 
-        | (Ind _ | Construct _ | Sort _) ->
-            List.iter (check_rec_call renv) l
+        | (Ind _ | Construct _) ->
+            List.iter (check_rec_call renv []) l
 
         | Var id ->
             begin
               match pi2 (lookup_named id renv.env) with
               | None ->
-                  List.iter (check_rec_call renv) l
+                  List.iter (check_rec_call renv []) l
               | Some c ->
-                  try List.iter (check_rec_call renv) l
-                  with (FixGuardError _) -> check_rec_call renv (applist(c,l))
+                  try List.iter (check_rec_call renv []) l
+                  with (FixGuardError _) -> 
+		    check_rec_call renv stack (applist(c,l))
             end
 
+	| Sort _ -> assert (l = [])
+
         (* l is not checked because it is considered as the meta's context *)
         | (Evar _ | Meta _) -> ()
 
-        | (App _ | LetIn _) -> assert false (* beta zeta reduction *)
+        | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
 
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if decr = 0 then
-      check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body
+      check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
     else
       match kind_of_term body with
 	| Lambda (x,a,b) ->
-	    check_rec_call renv a;
+	    check_rec_call renv [] a;
             let renv' = push_var_renv renv (x,a) in
-	    check_nested_fix_body renv' (decr-1) recArgsDecrArg b
+	      check_nested_fix_body renv' (decr-1) recArgsDecrArg b
 	| _ -> anomaly "Not enough abstractions in fix body"
-
+	    
   in
-  check_rec_call renv def
+  check_rec_call renv [] def
 
 let judgment_of_fixpoint (_, types, bodies) =
   array_map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies
@@ -829,7 +826,7 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
   let (minds, rdef) = inductive_of_mutfix env fix in
   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
+    let renv = make_renv fenv nvect.(i) minds.(i) in
     try check_one_fix renv nvect body
     with FixGuardError (fixenv,err) ->
       error_ill_formed_rec_body fixenv err names i
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 3212b8eed..202b1aa4c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -101,14 +101,11 @@ type guard_env =
   { env     : env;
     (** dB of last fixpoint *)
     rel_min : int;
-    (** inductive of recarg of each fixpoint *)
-    inds    : inductive array;
-    (** the recarg information of inductive family *)
-    recvec  : wf_paths array;
     (** dB of variables denoting subterms *)
     genv    : subterm_spec Lazy.t list;
   }
 
-val subterm_specif : guard_env -> constr -> subterm_spec
-val case_branches_specif : guard_env -> subterm_spec Lazy.t -> case_info ->
-  constr array -> (guard_env * constr) array
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
+
+val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
+
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6a18f72d5..7e910c360 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -294,9 +294,9 @@ let add_mind dir l mie senv =
   check_label l senv.labset;
     (* TODO: when we will allow reorderings we will have to verify
        all labels *)
-  let mib = translate_mind senv.env mie in
-  let senv' = add_constraints mib.mind_constraints senv in
   let kn = make_mind senv.modinfo.modpath dir l in
+  let mib = translate_mind senv.env kn mie in
+  let senv' = add_constraints mib.mind_constraints senv in
   let env'' = Environ.add_mind kn mib senv'.env in
   kn, { old = senv'.old;
 	env = env'';
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index da3393065..2189db264 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -138,4 +138,4 @@ let translate_recipe env kn r =
 
 (* Insertion of inductive types. *)
 
-let translate_mind env mie = check_inductive env mie
+let translate_mind env kn mie = check_inductive env kn mie
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 49463e75a..dbf479a0c 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -31,7 +31,7 @@ val build_constant_declaration : env -> 'a ->
 val translate_constant : env -> constant -> constant_entry -> constant_body
 
 val translate_mind :
-  env -> mutual_inductive_entry -> mutual_inductive_body
+  env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
 
 val translate_recipe :
   env -> constant -> Cooking.recipe -> constant_body
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 77b69bb88..c9f9fe7ad 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -18,7 +18,7 @@ type guard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
   | RecursionNotOnInductiveType of constr
-  | RecursionOnIllegalTerm of int * constr * int list * int list
+  | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
   | CodomainNotInductiveType of constr
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index dabff8360..3a6ad4bb1 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -18,7 +18,7 @@ type guard_error =
   (** Fixpoints *)
   | NotEnoughAbstractionInFixBody
   | RecursionNotOnInductiveType of constr
-  | RecursionOnIllegalTerm of int * constr * int list * int list
+  | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (** CoFixpoints *)
   | CodomainNotInductiveType of constr