Merge branch 'reduction-flags' into trunk

Was PR#231: Separate flags for fix/cofix/match reduction and clean reduction
function names, itself a revision of PR#117: Isolating flags for cofix/fix
reduction + adjusting names of reduction functions to what they do

19 files changed, 133 insertions, 163 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 78c218a509..c39a57012b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1708,7 +1708,7 @@ let build_inversion_problem loc env sigma tms t =
     let id = next_name_away (named_hd env t Anonymous) avoid in
     PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
-    match kind_of_term (whd_betadeltaiota env sigma t) with
+    match kind_of_term (whd_all env sigma t) with
     | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc
     | App (f,v) when isConstruct f ->
 	let cstr,u = destConstruct f in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index afd86420e9..1321474871 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -156,7 +156,7 @@ let strip_appl head stack =
 
 (* Tests if fixpoint reduction is possible. *)
 let fixp_reducible flgs ((reci,i),_) stk =
-  if red_set flgs fIOTA then
+  if red_set flgs fFIX then
     match stk with
       | APP(appl,_) ->
           Array.length appl > reci.(i) &&
@@ -168,7 +168,7 @@ let fixp_reducible flgs ((reci,i),_) stk =
     false
 
 let cofixp_reducible flgs _ stk =
-  if red_set flgs fIOTA then
+  if red_set flgs fCOFIX then
     match stk with
       | (CASE _ | APP(_,CASE _)) -> true
       | _ -> false
@@ -296,19 +296,19 @@ and cbv_stack_value info env = function
 
     (* constructor in a Case -> IOTA *)
     | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk)))
-            when red_set (info_flags info) fIOTA ->
+            when red_set (info_flags info) fMATCH ->
 	let cargs =
           Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
         cbv_stack_term info (stack_app cargs stk) env br.(n-1)
 
     (* constructor of arity 0 in a Case -> IOTA *)
     | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk))
-            when red_set (info_flags info) fIOTA ->
+            when red_set (info_flags info) fMATCH ->
                     cbv_stack_term info stk env br.(n-1)
 
     (* constructor in a Projection -> IOTA *)
     | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
-        when red_set (info_flags info) fIOTA && Projection.unfolded p ->
+        when red_set (info_flags info) fMATCH && Projection.unfolded p ->
       let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
 	cbv_stack_value info env (strip_appl arg stk)
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index d3d4201f57..5fb6c130eb 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -297,7 +297,7 @@ let lookup_path_to_sort_from env sigma s =
 
 let get_coercion_constructor env coe =
   let c, _ =
-    Reductionops.whd_betadeltaiota_stack env Evd.empty coe.coe_value
+    Reductionops.whd_all_stack env Evd.empty coe.coe_value
   in
   match kind_of_term c with
   | Construct (cstr,u) ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 65d79bcc85..704559dd73 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -63,7 +63,7 @@ let apply_coercion_args env evd check isproj argl funj =
 	{ uj_val = applist (j_val funj,argl);
 	  uj_type = typ }
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
-      match kind_of_term (whd_betadeltaiota env evd typ) with
+      match kind_of_term (whd_all env evd typ) with
       | Prod (_,c1,c2) ->
         if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then
 	  raise NoCoercion;
@@ -116,7 +116,7 @@ let disc_subset x =
 
 exception NoSubtacCoercion
   
-let hnf env evd c = whd_betadeltaiota env evd c
+let hnf env evd c = whd_all env evd c
 let hnf_nodelta env evd c = whd_betaiota evd c
 
 let lift_args n sign =
@@ -374,7 +374,7 @@ let apply_coercion env sigma p hj typ_cl =
 
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
 let inh_app_fun_core env evd j =
-  let t = whd_betadeltaiota env evd j.uj_type in
+  let t = whd_all env evd j.uj_type in
     match kind_of_term t with
     | Prod (_,_,_) -> (evd,j)
     | Evar ev ->
@@ -415,7 +415,7 @@ let inh_tosort_force loc env evd j =
     error_not_a_type_loc loc env evd j
 
 let inh_coerce_to_sort loc env evd j =
-  let typ = whd_betadeltaiota env evd j.uj_type in
+  let typ = whd_all env evd j.uj_type in
     match kind_of_term typ with
     | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
     | Evar ev when not (is_defined evd (fst ev)) ->
@@ -467,8 +467,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
       match
-      kind_of_term (whd_betadeltaiota env evd t),
-      kind_of_term (whd_betadeltaiota env evd c1)
+      kind_of_term (whd_all env evd t),
+      kind_of_term (whd_all env evd c1)
       with
       | Prod (name,t1,t2), Prod (_,u1,u2) ->
           (* Conversion did not work, we may succeed with a coercion. *)
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index d349cf8216..f9ab75cea9 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -78,7 +78,7 @@ let define_pure_evar_as_product evd evk =
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
   let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
-  let concl = Reductionops.whd_betadeltaiota evenv evd evi.evar_concl in
+  let concl = Reductionops.whd_all evenv evd evi.evar_concl in
   let s = destSort concl in
   let evd1,(dom,u1) =
     let evd = Sigma.Unsafe.of_evar_map evd in
@@ -131,7 +131,7 @@ let define_pure_evar_as_lambda env evd evk =
   let open Context.Named.Declaration in
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
-  let typ = Reductionops.whd_betadeltaiota evenv evd (evar_concl evi) in
+  let typ = Reductionops.whd_all evenv evd (evar_concl evi) in
   let evd1,(na,dom,rng) = match kind_of_term typ with
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
@@ -169,7 +169,7 @@ let define_evar_as_sort env evd (ev,args) =
   let evd, u = new_univ_variable univ_rigid evd in
   let evi = Evd.find_undefined evd ev in 
   let s = Type u in
-  let concl = Reductionops.whd_betadeltaiota (evar_env evi) evd evi.evar_concl in
+  let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in
   let sort = destSort concl in
   let evd' = Evd.define ev (mkSort s) evd in
   Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
@@ -181,10 +181,10 @@ let define_evar_as_sort env evd (ev,args) =
 
 let split_tycon loc env evd tycon =
   let rec real_split evd c =
-    let t = Reductionops.whd_betadeltaiota env evd c in
+    let t = Reductionops.whd_all env evd c in
       match kind_of_term t with
 	| Prod (na,dom,rng) -> evd, (na, dom, rng)
-	| Evar ev (* ev is undefined because of whd_betadeltaiota *) ->
+	| Evar ev (* ev is undefined because of whd_all *) ->
 	    let (evd',prod) = define_evar_as_product evd ev in
 	    let (_,dom,rng) = destProd prod in
 	      evd',(Anonymous, dom, rng)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 455a7dbd69..77b0c67ad5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -140,7 +140,7 @@ let recheck_applications conv_algo env evdref t =
        let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
        let rec aux i ty =
 	 if i < Array.length argsty then
-	 match kind_of_term (whd_betadeltaiota env !evdref ty) with
+	 match kind_of_term (whd_all env !evdref ty) with
 	 | Prod (na, dom, codom) ->
 	    (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
 	     | Success evd -> evdref := evd;
@@ -520,7 +520,7 @@ let solve_pattern_eqn env l c =
     l c in
   (* Warning: we may miss some opportunity to eta-reduce more since c'
      is not in normal form *)
-  whd_eta c'
+  shrink_eta c'
 
 (*****************************************)
 (* Refining/solving unification problems *)
@@ -797,7 +797,7 @@ let rec do_projection_effects define_fun env ty evd = function
       let evd = Evd.define evk (mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
       let evd = do_projection_effects define_fun env ty evd p in
-      let ty = whd_betadeltaiota env evd (Lazy.force ty) in
+      let ty = whd_all env evd (Lazy.force ty) in
       if not (isSort ty) then
         (* Don't try to instantiate if a sort because if evar_concl is an
            evar it may commit to a univ level which is not the right
@@ -1553,7 +1553,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
         raise e
     | OccurCheckIn (evd,rhs) ->
         (* last chance: rhs actually reduces to ev *)
-        let c = whd_betadeltaiota env evd rhs in
+        let c = whd_all env evd rhs in
         match kind_of_term c with
         | Evar (evk',argsv2) when Evar.equal evk evk' ->
 	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index fc38e98c63..866b2b495d 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -151,7 +151,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
   let nparams = List.length vargs in
   let process_pos env depK pk =
     let rec prec env i sign p =
-      let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
+      let p',largs = whd_allnolet_stack env sigma p in
       match kind_of_term p' with
 	| Prod (n,t,c) ->
 	    let d = LocalAssum (n,t) in
@@ -168,7 +168,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
             else
 	      base
       	| _ ->
-	   let t' = whd_betadeltaiota env sigma p in
+	   let t' = whd_all env sigma p in
 	   if Term.eq_constr p' t' then assert false
 	   else prec env i sign t'
     in
@@ -227,7 +227,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
   let process_pos env fk  =
     let rec prec env i hyps p =
-      let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
+      let p',largs = whd_allnolet_stack env sigma p in
       match kind_of_term p' with
 	| Prod (n,t,c) ->
 	    let d = LocalAssum (n,t) in
@@ -240,7 +240,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
             and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in
             applist(lift i fk,realargs@[arg])
      	| _ ->
-	   let t' = whd_betadeltaiota env sigma p in
+	   let t' = whd_all env sigma p in
 	     if Term.eq_constr t' p' then assert false
 	     else prec env i hyps t'
     in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 403dcfd1a3..6be6a2d3a2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -417,7 +417,7 @@ let extract_mrectype t =
     | _ -> raise Not_found
 
 let find_mrectype_vect env sigma c =
-  let (t, l) = decompose_appvect (whd_betadeltaiota env sigma c) in
+  let (t, l) = decompose_appvect (whd_all env sigma c) in
   match kind_of_term t with
     | Ind ind -> (ind, l)
     | _ -> raise Not_found
@@ -426,7 +426,7 @@ let find_mrectype env sigma c =
   let (ind, v) = find_mrectype_vect env sigma c in (ind, Array.to_list v)
 
 let find_rectype env sigma c =
-  let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
+  let (t, l) = decompose_app (whd_all env sigma c) in
   match kind_of_term t with
     | Ind (ind,u as indu) ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -436,7 +436,7 @@ let find_rectype env sigma c =
     | _ -> raise Not_found
 
 let find_inductive env sigma c =
-  let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
+  let (t, l) = decompose_app (whd_all env sigma c) in
   match kind_of_term t with
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
@@ -444,7 +444,7 @@ let find_inductive env sigma c =
     | _ -> raise Not_found
 
 let find_coinductive env sigma c =
-  let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
+  let (t, l) = decompose_app (whd_all env sigma c) in
   match kind_of_term t with
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
@@ -458,7 +458,7 @@ let find_coinductive env sigma c =
 
 let is_predicate_explicitly_dep env pred arsign =
   let rec srec env pval arsign =
-    let pv' = whd_betadeltaiota env Evd.empty pval in
+    let pv' = whd_all env Evd.empty pval in
     match kind_of_term pv', arsign with
       | Lambda (na,t,b), (LocalAssum _)::arsign ->
 	  srec (push_rel_assum (na,t) env) b arsign
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 2a5e999651..e537a3c0ae 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -35,13 +35,13 @@ let invert_tag cst tag reloc_tbl =
   with Find_at j -> (j+1)
 
 let decompose_prod env t =
-  let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
+  let (name,dom,codom as res) = destProd (whd_all env t) in
   match name with
   | Anonymous -> (Name (id_of_string "x"),dom,codom)
   | _ -> res
 
 let app_type env c =
-  let t = whd_betadeltaiota env c in
+  let t = whd_all env c in
   try destApp t with DestKO -> (t,[||])
 
  
@@ -289,7 +289,7 @@ and nf_atom_type env atom =
       let pT = 
 	hnf_prod_applist env 
 	  (Inductiveops.type_of_inductive env ind) (Array.to_list params) in
-      let pT = whd_betadeltaiota env pT in
+      let pT = whd_all env pT in
       let dep, p = nf_predicate env ind mip params p pT in
       (* Calcul du type des branches *)
       let btypes = build_branches_type env (fst ind) mib mip u params dep p in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b6a57785a1..38defe9510 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -675,7 +675,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       | c::rest ->
 	let argloc = loc_of_glob_constr c in
 	let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in
-        let resty = whd_betadeltaiota env !evdref resj.uj_type in
+        let resty = whd_all env !evdref resj.uj_type in
       	  match kind_of_term resty with
 	  | Prod (na,c1,c2) ->
 	    let tycon = Some c1 in
@@ -1017,7 +1017,7 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function
            let s =
 	     let sigma =  !evdref in
 	     let t = Retyping.get_type_of env sigma v in
-	       match kind_of_term (whd_betadeltaiota env sigma t) with
+	       match kind_of_term (whd_all env sigma t) with
                | Sort s -> s
                | Evar ev when is_Type (existential_type sigma ev) ->
 		   evd_comb1 (define_evar_as_sort env) evdref ev
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 2959bd7c84..95c6725f3c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -326,7 +326,7 @@ let is_open_canonical_projection env sigma (c,args) =
     (** Check if there is some canonical projection attached to this structure *)
     let _ = Refmap.find ref !object_table in
     try
-      let arg = whd_betadeltaiota env sigma (Stack.nth args n) in
+      let arg = whd_all env sigma (Stack.nth args n) in
       let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in
       not (isConstruct hd)
     with Failure _ -> false
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index c188995a84..db5879174d 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -14,7 +14,9 @@ let make_red_flag l =
   let rec add_flag red = function
     | [] -> red
     | FBeta :: lf -> add_flag { red with rBeta = true } lf
-    | FIota :: lf -> add_flag { red with rIota = true } lf
+    | FMatch :: lf -> add_flag { red with rMatch = true } lf
+    | FFix :: lf -> add_flag { red with rFix = true } lf
+    | FCofix :: lf -> add_flag { red with rCofix = true } lf
     | FZeta :: lf -> add_flag { red with rZeta = true } lf
     | FConst l :: lf ->
 	if red.rDelta then
@@ -30,9 +32,11 @@ let make_red_flag l =
           lf
   in
   add_flag
-    {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
+    {rBeta = false; rMatch = false; rFix = false; rCofix = false;
+     rZeta = false; rDelta = false; rConst = []}
     l
 
 
 let all_flags =
-  {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
+  {rBeta = true; rMatch = true; rFix = true; rCofix = true;
+   rZeta = true; rDelta = true; rConst = []}
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 79cb7a2f67..29b448caa3 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -619,23 +619,7 @@ let rec strong_prodspine redfun sigma c =
 (*** Reduction using bindingss ***)
 (*************************************)
 
-(* Local *)
-let nored = Closure.RedFlags.no_red
-let beta = Closure.beta
 let eta = Closure.RedFlags.mkflags [Closure.RedFlags.fETA]
-let zeta = Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]
-let betaiota = Closure.betaiota
-let betaiotazeta = Closure.betaiotazeta
-
-(* Contextual *)
-let delta = Closure.RedFlags.mkflags [Closure.RedFlags.fDELTA]
-let betalet = Closure.RedFlags.mkflags [Closure.RedFlags.fBETA;Closure.RedFlags.fZETA]
-let betaetalet = Closure.RedFlags.red_add betalet Closure.RedFlags.fETA
-let betadelta = Closure.RedFlags.red_add betalet Closure.RedFlags.fDELTA
-let betadeltaeta = Closure.RedFlags.red_add betadelta Closure.RedFlags.fETA
-let betadeltaiota = Closure.RedFlags.red_add betadelta Closure.RedFlags.fIOTA
-let betadeltaiota_nolet = Closure.betadeltaiotanolet
-let betadeltaiotaeta = Closure.RedFlags.red_add betadeltaiota Closure.RedFlags.fETA
 
 (* Beta Reduction tools *)
 
@@ -950,13 +934,15 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 	whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s'))
 
     | Construct ((ind,c),u) ->
-      if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
+      let use_match = Closure.RedFlags.red_set flags Closure.RedFlags.fMATCH in
+      let use_fix = Closure.RedFlags.red_set flags Closure.RedFlags.fFIX in
+      if use_match || use_fix then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, (Stack.Case(ci, _, lf,_)::s') when use_match ->
 	  whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
-	|args, (Stack.Proj (n,m,p,_)::s') ->
+	|args, (Stack.Proj (n,m,p,_)::s') when use_match ->
 	  whrec Cst_stack.empty (Stack.nth args (n+m), s')
-	|args, (Stack.Fix (f,s',cst_l)::s'') ->
+	|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
 	  let x' = Stack.zip(x,args) in
 	  let out_sk = s' @ (Stack.append_app [|x'|] s'') in
 	  reduce_and_refold_fix whrec env cst_l f out_sk
@@ -988,11 +974,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 		 Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''')
 	  end
 	|_, (Stack.App _|Stack.Update _|Stack.Shift _)::_ -> assert false
-	|_, [] -> fold ()
+	|_, _ -> fold ()
       else fold ()
 
     | CoFix cofix ->
-      if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
+      if Closure.RedFlags.red_set flags Closure.RedFlags.fCOFIX then
 	match Stack.strip_app stack with
 	|args, ((Stack.Case _ |Stack.Proj _)::s') ->
 	  reduce_and_refold_cofix whrec env cst_l cofix stack
@@ -1059,21 +1045,23 @@ let local_whd_state_gen flags sigma =
       | None -> s)
 
     | Construct ((ind,c),u) ->
-      if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
+      let use_match = Closure.RedFlags.red_set flags Closure.RedFlags.fMATCH in
+      let use_fix = Closure.RedFlags.red_set flags Closure.RedFlags.fFIX in
+      if use_match || use_fix then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, (Stack.Case(ci, _, lf,_)::s') when use_match ->
 	  whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
-	|args, (Stack.Proj (n,m,p,_) :: s') ->
+	|args, (Stack.Proj (n,m,p,_) :: s') when use_match ->
 	  whrec (Stack.nth args (n+m), s')
-	|args, (Stack.Fix (f,s',cst)::s'') ->
+	|args, (Stack.Fix (f,s',cst)::s'') when use_fix ->
 	  let x' = Stack.zip(x,args) in
 	  whrec (contract_fix f, s' @ (Stack.append_app [|x'|] s''))
 	|_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false
-	|_, [] -> s
+	|_, _ -> s
       else s
 
     | CoFix cofix ->
-      if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
+      if Closure.RedFlags.red_set flags Closure.RedFlags.fCOFIX then
 	match Stack.strip_app stack with
 	|args, ((Stack.Case _ | Stack.Proj _)::s') ->
 	  whrec (contract_cofix cofix, stack)
@@ -1105,79 +1093,64 @@ let red_of_state_red f sigma x =
 
 (* 0. No Reduction Functions *)
 
-let whd_nored_state = local_whd_state_gen nored
+let whd_nored_state = local_whd_state_gen Closure.nored
 let whd_nored_stack = stack_red_of_state_red whd_nored_state
 let whd_nored = red_of_state_red whd_nored_state
 
 (* 1. Beta Reduction Functions *)
 
-let whd_beta_state = local_whd_state_gen beta
+let whd_beta_state = local_whd_state_gen Closure.beta
 let whd_beta_stack = stack_red_of_state_red whd_beta_state
 let whd_beta = red_of_state_red whd_beta_state
 
-(* Nouveau ! *)
-let whd_betaetalet_state = local_whd_state_gen betaetalet
-let whd_betaetalet_stack = stack_red_of_state_red whd_betaetalet_state
-let whd_betaetalet = red_of_state_red whd_betaetalet_state
-
-let whd_betalet_state = local_whd_state_gen betalet
+let whd_betalet_state = local_whd_state_gen Closure.betazeta
 let whd_betalet_stack = stack_red_of_state_red whd_betalet_state
 let whd_betalet = red_of_state_red whd_betalet_state
 
 (* 2. Delta Reduction Functions *)
 
-let whd_delta_state e = raw_whd_state_gen delta e
+let whd_delta_state e = raw_whd_state_gen Closure.delta e
 let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env)
 let whd_delta env = red_of_state_red  (whd_delta_state env)
 
-let whd_betadelta_state e = raw_whd_state_gen betadelta e
-let whd_betadelta_stack env =
-  stack_red_of_state_red (whd_betadelta_state env)
-let whd_betadelta env =
-  red_of_state_red (whd_betadelta_state env)
-
+let whd_betadeltazeta_state e = raw_whd_state_gen Closure.betadeltazeta e
+let whd_betadeltazeta_stack env =
+  stack_red_of_state_red (whd_betadeltazeta_state env)
+let whd_betadeltazeta env =
+  red_of_state_red (whd_betadeltazeta_state env)
 
-let whd_betadeltaeta_state e = raw_whd_state_gen betadeltaeta e
-let whd_betadeltaeta_stack env =
-  stack_red_of_state_red (whd_betadeltaeta_state env)
-let whd_betadeltaeta env =
-  red_of_state_red (whd_betadeltaeta_state env)
 
 (* 3. Iota reduction Functions *)
 
-let whd_betaiota_state = local_whd_state_gen betaiota
+let whd_betaiota_state = local_whd_state_gen Closure.betaiota
 let whd_betaiota_stack = stack_red_of_state_red whd_betaiota_state
 let whd_betaiota = red_of_state_red whd_betaiota_state
 
-let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta
+let whd_betaiotazeta_state = local_whd_state_gen Closure.betaiotazeta
 let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state
 let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
 
-let whd_betadeltaiota_state env = raw_whd_state_gen betadeltaiota env
-let whd_betadeltaiota_stack env =
-  stack_red_of_state_red (whd_betadeltaiota_state env)
-let whd_betadeltaiota env =
-  red_of_state_red (whd_betadeltaiota_state env)
-
-let whd_betadeltaiotaeta_state env = raw_whd_state_gen betadeltaiotaeta env
-let whd_betadeltaiotaeta_stack env =
-  stack_red_of_state_red (whd_betadeltaiotaeta_state env)
-let whd_betadeltaiotaeta env =
-  red_of_state_red (whd_betadeltaiotaeta_state env)
+let whd_all_state env = raw_whd_state_gen Closure.all env
+let whd_all_stack env =
+  stack_red_of_state_red (whd_all_state env)
+let whd_all env =
+  red_of_state_red (whd_all_state env)
 
-let whd_betadeltaiota_nolet_state env = raw_whd_state_gen betadeltaiota_nolet env
-let whd_betadeltaiota_nolet_stack env =
-  stack_red_of_state_red (whd_betadeltaiota_nolet_state env)
-let whd_betadeltaiota_nolet env =
-  red_of_state_red (whd_betadeltaiota_nolet_state env)
+let whd_allnolet_state env = raw_whd_state_gen Closure.allnolet env
+let whd_allnolet_stack env =
+  stack_red_of_state_red (whd_allnolet_state env)
+let whd_allnolet env =
+  red_of_state_red (whd_allnolet_state env)
 
-(* 4. Eta reduction Functions *)
+(* 4. Ad-hoc eta reduction, does not subsitute evars *)
 
-let whd_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty))
+let shrink_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty))
 
 (* 5. Zeta Reduction Functions *)
 
-let whd_zeta c = Stack.zip (local_whd_state_gen zeta Evd.empty (c,Stack.empty))
+let whd_zeta_state = local_whd_state_gen Closure.zeta
+let whd_zeta_stack = stack_red_of_state_red whd_zeta_state
+let whd_zeta = red_of_state_red whd_zeta_state
 
 (****************************************************************************)
 (*                   Reduction Functions                                    *)
@@ -1201,8 +1174,8 @@ let clos_norm_flags flgs env sigma t =
 let nf_beta = clos_norm_flags Closure.beta (Global.env ())
 let nf_betaiota = clos_norm_flags Closure.betaiota (Global.env ())
 let nf_betaiotazeta = clos_norm_flags Closure.betaiotazeta (Global.env ())
-let nf_betadeltaiota env sigma =
-  clos_norm_flags Closure.betadeltaiota env sigma
+let nf_all env sigma =
+  clos_norm_flags Closure.all env sigma
 
 
 (********************************************************************)
@@ -1397,7 +1370,7 @@ let instance sigma s c =
  * error message. *)
 
 let hnf_prod_app env sigma t n =
-  match kind_of_term (whd_betadeltaiota env sigma t) with
+  match kind_of_term (whd_all env sigma t) with
     | Prod (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
 
@@ -1408,7 +1381,7 @@ let hnf_prod_applist env sigma t nl =
   List.fold_left (hnf_prod_app env sigma) t nl
 
 let hnf_lam_app env sigma t n =
-  match kind_of_term (whd_betadeltaiota env sigma t) with
+  match kind_of_term (whd_all env sigma t) with
     | Lambda (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
 
@@ -1420,7 +1393,7 @@ let hnf_lam_applist env sigma t nl =
 
 let splay_prod env sigma =
   let rec decrec env m c =
-    let t = whd_betadeltaiota env sigma c in
+    let t = whd_all env sigma c in
     match kind_of_term t with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (LocalAssum (n,a)) env)
@@ -1431,7 +1404,7 @@ let splay_prod env sigma =
 
 let splay_lam env sigma =
   let rec decrec env m c =
-    let t = whd_betadeltaiota env sigma c in
+    let t = whd_all env sigma c in
     match kind_of_term t with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (LocalAssum (n,a)) env)
@@ -1442,7 +1415,7 @@ let splay_lam env sigma =
 
 let splay_prod_assum env sigma =
   let rec prodec_rec env l c =
-    let t = whd_betadeltaiota_nolet env sigma c in
+    let t = whd_allnolet env sigma c in
     match kind_of_term t with
     | Prod (x,t,c)  ->
 	prodec_rec (push_rel (LocalAssum (x,t)) env)
@@ -1452,7 +1425,7 @@ let splay_prod_assum env sigma =
 	  (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> 
-      let t' = whd_betadeltaiota env sigma t in
+      let t' = whd_all env sigma t in
 	if Term.eq_constr t t' then l,t
 	else prodec_rec env l t'
   in
@@ -1468,7 +1441,7 @@ let sort_of_arity env sigma c = snd (splay_arity env sigma c)
 
 let splay_prod_n env sigma n =
   let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
-    match kind_of_term (whd_betadeltaiota env sigma c) with
+    match kind_of_term (whd_all env sigma c) with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (LocalAssum (n,a)) env)
 	    (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
@@ -1478,7 +1451,7 @@ let splay_prod_n env sigma n =
 
 let splay_lam_n env sigma n =
   let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
-    match kind_of_term (whd_betadeltaiota env sigma c) with
+    match kind_of_term (whd_all env sigma c) with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (LocalAssum (n,a)) env)
 	    (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
@@ -1487,7 +1460,7 @@ let splay_lam_n env sigma n =
   decrec env n Context.Rel.empty
 
 let is_sort env sigma t =
-  match kind_of_term (whd_betadeltaiota env sigma t) with
+  match kind_of_term (whd_all env sigma t) with
   | Sort s -> true
   | _ -> false
 
@@ -1496,19 +1469,19 @@ let is_sort env sigma t =
 
 let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
   let rec whrec csts s =
-    let (t, stack as s),csts' = whd_state_gen ~csts false betaiota env sigma s in
+    let (t, stack as s),csts' = whd_state_gen ~csts false Closure.betaiota env sigma s in
     match Stack.strip_app stack with
       |args, (Stack.Case _ :: _ as stack') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
-	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
+	  (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in
 	if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |args, (Stack.Fix _ :: _ as stack') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
-	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
+	  (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in
 	if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |args, (Stack.Proj (n,m,p,_) :: stack'') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
-	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
+	  (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in
 	if isConstruct t_o then
 	  whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
 	else s,csts'
@@ -1517,7 +1490,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 
 let find_conclusion env sigma =
   let rec decrec env c =
-    let t = whd_betadeltaiota env sigma c in
+    let t = whd_all env sigma c in
     match kind_of_term t with
       | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
       | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b38252e971..fdfa77412e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -148,7 +148,7 @@ val clos_norm_flags : Closure.RedFlags.reds -> reduction_function
 val nf_beta : local_reduction_function
 val nf_betaiota : local_reduction_function
 val nf_betaiotazeta : local_reduction_function
-val nf_betadeltaiota : reduction_function
+val nf_all : reduction_function
 val nf_evar : evar_map -> constr -> constr
 
 (** Lazy strategy, weak head reduction *)
@@ -158,9 +158,8 @@ val whd_nored : local_reduction_function
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betaiotazeta : local_reduction_function
-val whd_betadeltaiota :  contextual_reduction_function
-val whd_betadeltaiota_nolet :  contextual_reduction_function
-val whd_betaetalet : local_reduction_function
+val whd_all :  contextual_reduction_function
+val whd_allnolet :  contextual_reduction_function
 val whd_betalet : local_reduction_function
 
 (** Removes cast and put into applicative form *)
@@ -168,18 +167,16 @@ val whd_nored_stack : local_stack_reduction_function
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
 val whd_betaiotazeta_stack : local_stack_reduction_function
-val whd_betadeltaiota_stack : contextual_stack_reduction_function
-val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function
-val whd_betaetalet_stack : local_stack_reduction_function
+val whd_all_stack : contextual_stack_reduction_function
+val whd_allnolet_stack : contextual_stack_reduction_function
 val whd_betalet_stack : local_stack_reduction_function
 
 val whd_nored_state : local_state_reduction_function
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
 val whd_betaiotazeta_state : local_state_reduction_function
-val whd_betadeltaiota_state : contextual_state_reduction_function
-val whd_betadeltaiota_nolet_state : contextual_state_reduction_function
-val whd_betaetalet_state : local_state_reduction_function
+val whd_all_state : contextual_state_reduction_function
+val whd_allnolet_state : contextual_state_reduction_function
 val whd_betalet_state : local_state_reduction_function
 
 (** {6 Head normal forms } *)
@@ -187,18 +184,14 @@ val whd_betalet_state : local_state_reduction_function
 val whd_delta_stack :  stack_reduction_function
 val whd_delta_state :  state_reduction_function
 val whd_delta :  reduction_function
-val whd_betadelta_stack :  stack_reduction_function
-val whd_betadelta_state :  state_reduction_function
-val whd_betadelta :  reduction_function
-val whd_betadeltaeta_stack :  stack_reduction_function
-val whd_betadeltaeta_state :  state_reduction_function
-val whd_betadeltaeta :  reduction_function
-val whd_betadeltaiotaeta_stack :  stack_reduction_function
-val whd_betadeltaiotaeta_state :  state_reduction_function
-val whd_betadeltaiotaeta :  reduction_function
-
-val whd_eta : constr -> constr
-val whd_zeta : constr -> constr
+val whd_betadeltazeta_stack :  stack_reduction_function
+val whd_betadeltazeta_state :  state_reduction_function
+val whd_betadeltazeta :  reduction_function
+val whd_zeta_stack : local_stack_reduction_function
+val whd_zeta_state : local_state_reduction_function
+val whd_zeta : local_reduction_function
+
+val shrink_eta : constr -> constr
 
 (** Various reduction functions *)
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 1a6f7832aa..5de540a000 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -62,7 +62,7 @@ let get_type_from_constraints env sigma t =
 let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
-      match kind_of_term (whd_betadeltaiota env sigma typ) with
+      match kind_of_term (whd_all env sigma typ) with
         | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest
         | _ -> retype_error NonFunctionalConstruction
 
@@ -71,7 +71,7 @@ let rec subst_type env sigma typ = function
 
 let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env n ar args =
-    match kind_of_term (whd_betadeltaiota env sigma ar), args with
+    match kind_of_term (whd_all env sigma ar), args with
     | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l
     | Sort s, [] -> s
     | _ -> retype_error NotASort
@@ -83,7 +83,7 @@ let type_of_var env id =
   with Not_found -> retype_error (BadVariable id)
 
 let decomp_sort env sigma t =
-  match kind_of_term (whd_betadeltaiota env sigma t) with
+  match kind_of_term (whd_all env sigma t) with
   | Sort s -> s
   | _ -> retype_error NotASort
 
@@ -113,7 +113,7 @@ let retype ?(polyprop=true) sigma =
         in
         let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
         let t = betazetaevar_applist sigma n p realargs in
-        (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
+        (match kind_of_term (whd_all env sigma (type_of env t)) with
           | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)
     | Lambda (name,c1,c2) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 7d2504004f..51a89966fe 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -257,7 +257,7 @@ let invert_name labs l na0 env sigma ref = function
 
 let compute_consteval_direct env sigma ref =
   let rec srec env n labs onlyproj c =
-    let c',l = whd_betadelta_stack env sigma c in
+    let c',l = whd_betadeltazeta_stack env sigma c in
     match kind_of_term c' with
       | Lambda (id,t,g) when List.is_empty l && not onlyproj ->
           let open Context.Rel.Declaration in
@@ -870,7 +870,7 @@ let red_product env sigma c =
  *)
 
 let whd_simpl_orelse_delta_but_fix_old env sigma c =
-  let whd_all = whd_betadeltaiota_state env sigma in
+  let whd_all = whd_all_state env sigma in
   let rec redrec (x, stack as s) =
     match kind_of_term x with
       | Lambda (na,t,c) ->
@@ -1125,7 +1125,7 @@ let cbv_norm_flags flags env sigma t =
 
 let cbv_beta = cbv_norm_flags beta empty_env
 let cbv_betaiota = cbv_norm_flags betaiota empty_env
-let cbv_betadeltaiota env sigma =  cbv_norm_flags betadeltaiota env sigma
+let cbv_betadeltaiota env sigma =  cbv_norm_flags all env sigma
 
 let compute = cbv_betadeltaiota
 
@@ -1186,7 +1186,7 @@ let reduce_to_ind_gen allow_product env sigma t =
       | _ ->
 	  (* Last chance: we allow to bypass the Opaque flag (as it
 	     was partially the case between V5.10 and V8.1 *)
-	  let t' = whd_betadeltaiota env sigma t in
+	  let t' = whd_all env sigma t in
 	  match kind_of_term (fst (decompose_app t')) with
 	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
 	    | _ -> errorlabstrm "" (str"Not an inductive product.")
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 52afa7f83a..8e44fb0082 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -36,7 +36,7 @@ let inductive_type_knowing_parameters env (ind,u) jl =
   Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
 
 let e_type_judgment env evdref j =
-  match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with
+  match kind_of_term (whd_all env !evdref j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
@@ -54,7 +54,7 @@ let e_judge_of_apply env evdref funj argjv =
       { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
         uj_type = typ }
   | hj::restjl ->
-      match kind_of_term (whd_betadeltaiota env !evdref typ) with
+      match kind_of_term (whd_all env !evdref typ) with
       | Prod (_,c1,c2) ->
 	 if Evarconv.e_cumul env evdref hj.uj_type c1 then
 	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
@@ -87,7 +87,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
   let allowed_sorts = elim_sorts specif in
   let error () = error_elim_arity env ind allowed_sorts c pj None in
   let rec srec env pt ar =
-    let pt' = whd_betadeltaiota env !evdref pt in
+    let pt' = whd_all env !evdref pt in
     match kind_of_term pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
         if not (Evarconv.e_cumul env evdref a1 a1') then error ();
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 21cf5548f2..5bb853b694 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1090,7 +1090,7 @@ let left = true
 let right = false
 
 let rec unify_with_eta keptside flags env sigma c1 c2 =
-(* Question: try whd_betadeltaiota on ci if not two lambdas? *)
+(* Question: try whd_all on ci if not two lambdas? *)
   match kind_of_term c1, kind_of_term c2 with
   | (Lambda (na,t1,c1'), Lambda (_,t2,c2')) ->
     let env' = push_rel_assum (na,t1) env in
@@ -1200,7 +1200,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
     if Int.equal n 0 then
       Sigma (c, evd, p)
     else
-      match kind_of_term (whd_betadeltaiota env (Sigma.to_evar_map evd) cty) with
+      match kind_of_term (whd_all env (Sigma.to_evar_map evd) cty) with
       | Prod (_,c1,c2) ->
         let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
@@ -1343,7 +1343,7 @@ let w_merge env with_types flags (evd,metas,evars) =
     	  else
             let evd' =
               if occur_meta_evd evd mv c then
-                if isMetaOf mv (whd_betadeltaiota env evd c) then evd
+                if isMetaOf mv (whd_all env evd c) then evd
                 else error_cannot_unify env evd (mkMeta mv,c)
               else
 	        meta_assign mv (c,(status,TypeProcessed)) evd in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 7ea9b90635..0b102f9218 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -24,7 +24,7 @@ open Context.Rel.Declaration
 let crazy_type =  mkSet
 
 let decompose_prod env t =
-  let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
+  let (name,dom,codom as res) = destProd (whd_all env t) in
   match name with
   | Anonymous -> (Name (Id.of_string "x"), dom, codom)
   | Name _ -> res
@@ -234,7 +234,7 @@ and nf_stk ?from:(from=0) env c t stk  =
       let params,realargs = Util.Array.chop nparams allargs in
       let pT =
 	hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
-      let pT = whd_betadeltaiota env pT in
+      let pT = whd_all env pT in
       let dep, p = nf_predicate env (ind,u) mip params (type_of_switch sw) pT in
       (* Calcul du type des branches *)
       let btypes = build_branches_type env ind mib mip u params dep p in