Nettoyage/restructuration des ensembles d'indicateurs de réductions

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

3 files changed, 257 insertions, 330 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index a09368fcd..81c1b7bcc 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -38,6 +38,13 @@ let stop() =
 	   'sTR" zeta="; 'iNT !zeta; 'sTR" evar="; 'iNT !evar;
            'sTR" iota="; 'iNT !iota; 'sTR" prune="; 'iNT !prune; 'sTR"]" >]
 
+let incr_cnt red cnt =
+  if red then begin
+    if !stats then incr cnt;
+    true
+  end else 
+    false
+
 let with_stats c =
   if !stats then begin
     reset();
@@ -51,6 +58,129 @@ type evaluable_global_reference =
   | EvalVarRef of identifier
   | EvalConstRef of section_path
 
+module type RedFlagsSig = sig
+  type reds
+  type red_kind
+  val fBETA : red_kind
+  val fEVAR : red_kind
+  val fDELTA : red_kind
+  val fIOTA : red_kind
+  val fZETA : red_kind
+  val fCONST : constant_path -> red_kind
+  val fCONSTBUT : constant_path -> red_kind
+  val fVAR : identifier -> red_kind
+  val fVARBUT : identifier -> red_kind
+  val no_red : reds
+  val red_add : reds -> red_kind -> reds
+  val mkflags : red_kind list -> reds
+  val red_set : reds -> red_kind -> bool
+  val red_get_const : reds -> bool * evaluable_global_reference list
+end
+
+module RedFlags = (struct
+
+  (* [r_const=(true,cl)] means all constants but those in [cl] *)
+  (* [r_const=(false,cl)] means only those in [cl] *)
+  (* [r_delta=true] just mean [r_const=(true,[])] *)
+
+  type reds = {
+    r_beta : bool;
+    r_delta : bool;
+    r_const : bool * constant_path list * identifier list;
+    r_zeta : bool;
+    r_evar : bool;
+    r_iota : bool }
+
+  type red_kind = BETA | DELTA | EVAR | IOTA | ZETA
+	      | CONST of constant_path | CONSTBUT of constant_path
+	      | VAR of identifier | VARBUT of identifier
+  let fBETA = BETA
+  let fDELTA = DELTA
+  let fEVAR = EVAR 
+  let fIOTA = IOTA
+  let fZETA = ZETA
+  let fCONST sp  = CONST sp
+  let fCONSTBUT sp = CONSTBUT sp
+  let fVAR id = VAR id
+  let fVARBUT id = VARBUT id
+  let no_red = {
+    r_beta = false;
+    r_delta = false;
+    r_const = false,[],[];
+    r_zeta = false;
+    r_evar = false;
+    r_iota = false }
+
+  let red_add red = function
+    | BETA -> { red with r_beta = true }
+    | DELTA ->
+	(match red.r_const with
+	   | _,_::_,[] | _,[],_::_ -> error "Conflict in the reduction flags"
+	   | _ -> { red with r_const = true,[],[]; r_delta = true })
+    | CONST sp ->
+	let (oldallbut,l1,l2) = red.r_const in
+	if oldallbut then error "Conflict in the reduction flags"
+	else { red with r_const = false, list_union [sp] l1, l2 }
+    | CONSTBUT sp ->
+	(match red.r_const with
+	   | (false,_::_,_ | false,_,_::_ | true,[],[]) ->
+	       error "Conflict in the reduction flags"
+	   | (_,l1,l2) -> { red with r_const = true, list_union [sp] l1, l2 })
+    | IOTA -> { red with r_iota = true }
+    | EVAR -> { red with r_evar = true }
+    | ZETA -> { red with r_zeta = true }
+    | VAR id ->
+	let (oldallbut,l1,l2) = red.r_const in
+	if oldallbut then error "Conflict in the reduction flags"
+	else { red with r_const = false, l1, list_union [id] l2 }
+    | VARBUT id ->
+	(match red.r_const with
+	   | (false,_::_,_ | false,_,_::_ | true,[],[]) ->
+	       error "Conflict in the reduction flags"
+	   | (_,l1,l2) -> { red with r_const = true, l1, list_union [id] l2 })
+
+  let mkflags = List.fold_left red_add no_red
+
+  let red_set red = function
+    | BETA -> incr_cnt red.r_beta beta
+    | CONST sp -> 
+	let (b,l,_) = red.r_const in
+	let c = List.mem sp l in
+	incr_cnt ((b & not c) or (c & not b)) delta
+    | VAR id -> (* En attendant d'avoir des sp pour les Var *)
+	let (b,_,l) = red.r_const in
+	let c = List.mem id l in
+	incr_cnt ((b & not c) or (c & not b)) delta
+    | ZETA -> incr_cnt red.r_zeta zeta
+    | EVAR -> incr_cnt red.r_zeta evar
+    | IOTA -> incr_cnt red.r_iota iota
+    | DELTA -> (* Used for Rel/Var defined in context *)
+	incr_cnt red.r_delta delta
+    | (CONSTBUT _ | VARBUT _) -> (* Not for internal use *)
+	failwith "not implemented"
+
+  let red_get_const red =
+    let b,l1,l2 = red.r_const in
+    let l1' = List.map (fun x -> EvalConstRef x) l1 in
+    let l2' = List.map (fun x -> EvalVarRef x) l2 in
+    b, l1' @ l2'
+
+end : RedFlagsSig)
+
+open RedFlags
+
+let betadeltaiota_red = mkflags [fBETA;fDELTA;fZETA;fEVAR;fIOTA]
+let betaiota_red = mkflags [fBETA;fIOTA]
+let beta_red = mkflags [fBETA]
+let betaiotazeta_red = mkflags [fBETA;fIOTA;fZETA]
+let unfold_red sp = 
+  let flag = match sp with
+    | EvalVarRef id -> fVAR id
+    | EvalConstRef sp -> fCONST sp
+  in (* Remove fZETA for finer behaviour ? *)
+  mkflags [fBETA;flag;fIOTA;fZETA]
+
+(************************* Obsolète
 (* [r_const=(true,cl)] means all constants but those in [cl] *)
 (* [r_const=(false,cl)] means only those in [cl] *)
 type reds = {
@@ -149,14 +279,6 @@ let rec red_add red = function
 	    { red with r_const = true, l1, list_union [cl] l2;
 		r_zeta = true; r_evar = true })
 
-
-let incr_cnt red cnt =
-  if red then begin
-    if !stats then incr cnt;
-    true
-  end else 
-    false
-
 let red_delta_set red =
   let b,_,_ = red.r_const in b
 
@@ -186,7 +308,7 @@ let red_get_const red =
   let l1' = List.map (fun x -> EvalConstRef x) l1 in
   let l2' = List.map (fun x -> EvalVarRef x) l2 in
   b, l1' @ l2'
-
+fin obsolète **************)
 (* specification of the reduction function *)
 
 type red_mode = UNIFORM | SIMPL | WITHBACK
@@ -820,30 +942,30 @@ and knht e t stk =
 (* Computes a normal form from the result of knh. *)
 let rec knr info m stk =
   match m.term with
-  | FLambda(_,_,_,f,e) when can_red info stk BETA ->
+  | FLambda(_,_,_,f,e) when can_red info stk fBETA ->
       (match get_arg m stk with
           (Some(depth,arg),s) -> knit info (subs_shift_cons(depth,e,arg)) f s
         | (None,s) -> (m,s))
-  | FFlex(FConst(sp,args)) when can_red info stk (CONST [sp]) ->
+  | FFlex(FConst(sp,args)) when can_red info stk (fCONST sp) ->
       let cst = (sp, Array.map term_of_fconstr args) in
       (match ref_value_cache info (ConstBinding cst) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FFlex(FEvar ev) when can_red info stk EVAR ->
+  | FFlex(FEvar ev) when can_red info stk fEVAR ->
 (* In the case of evars, if it is not defined, then we do not set the
    flag to Norm, because it may be instantiated later on *)
       (match ref_value_cache info (EvarBinding ev) with
           Some v -> kni info v stk
         | None -> (m,stk))
-  | FFlex(FVar id) when can_red info stk (VAR id) ->
+  | FFlex(FVar id) when can_red info stk (fVAR id) ->
       (match ref_value_cache info (VarBinding id) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FFlex(FFarRel k) when can_red info stk DELTA ->
+  | FFlex(FFarRel k) when can_red info stk fDELTA ->
       (match ref_value_cache info (FarRelBinding k) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FConstruct((sp,c),args) when can_red info stk IOTA ->
+  | FConstruct((sp,c),args) when can_red info stk fIOTA ->
       (match strip_update_shift_app m stk with
           (depth, args, Zcase((cn,_),_,br)::s) ->
             let npar = stack_args_size args - cn.(c-1) in
@@ -856,13 +978,13 @@ let rec knr info m stk =
             let efx = contract_fix_vect fx.term in
             kni info efx stk'
         | (_,args,s) -> (m,args@s))
-  | FCoFix _ when can_red info stk IOTA ->
+  | FCoFix _ when can_red info stk fIOTA ->
       (match strip_update_shift_app m stk with
           (_, args, ((Zcase((cn,_),_,br)::_) as stk')) ->
             let efx = contract_fix_vect m.term in
             kni info efx (args@stk')
         | (_,args,s) -> (m,args@s))
-  | FLetIn (_,v,_,_,bd,e) when can_red info stk ZETA ->
+  | FLetIn (_,v,_,_,bd,e) when can_red info stk fZETA ->
       knit info (subs_cons(v,e)) bd stk
   | _ -> (m,stk)
 
diff --git a/kernel/closure.mli b/kernel/closure.mli
index e40167918..6f5afc4e2 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -32,7 +32,8 @@ type evaluable_global_reference =
   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of 
   a LetIn expression is Letin reduction *)
 
-type red_kind =
+(*
+type red_kind = 
   | BETA
   | DELTA
   | ZETA
@@ -42,25 +43,50 @@ type red_kind =
   | CONSTBUT of section_path list
   | VAR of identifier
   | VARBUT of identifier
-
+*)
 (* Sets of reduction kinds. *)
-type reds
+module type RedFlagsSig = sig
+  type reds
+  type red_kind
+
+  (* The different kind of reduction *)
+  (* Const/Var means the reference as argument should be unfolded *)
+  (* Constbut/Varbut means all references except the ones as argument
+     of Constbut/Varbut should be unfolded (there may be several such
+     Constbut/Varbut *)
+  val fBETA : red_kind
+  val fEVAR : red_kind
+  val fDELTA : red_kind
+  val fIOTA : red_kind
+  val fZETA : red_kind
+  val fCONST : constant_path -> red_kind
+  val fCONSTBUT : constant_path -> red_kind
+  val fVAR : identifier -> red_kind
+  val fVARBUT : identifier -> red_kind
+
+  (* No reduction at all *)
+  val no_red : reds
+
+  (* Adds a reduction kind to a set *)
+  val red_add : reds -> red_kind -> reds
+
+  (* Build a reduction set from scratch = iter [red_add] on [no_red] *)
+  val mkflags : red_kind list -> reds
+
+  (* Tests if a reduction kind is set *)
+  val red_set : reds -> red_kind -> bool
+
+  (* Gives the constant list *)
+  val red_get_const : reds -> bool * evaluable_global_reference list
+end
+
+module RedFlags : RedFlagsSig
+open RedFlags
 
-val no_red : reds
 val beta_red : reds
 val betaiota_red : reds
 val betadeltaiota_red : reds
 val betaiotazeta_red : reds
-val unfold_red : evaluable_global_reference -> reds
-
-(* Tests if a reduction kind is set *)
-val red_set : reds -> red_kind -> bool
-
-(* Adds a reduction kind to a set *)
-val red_add : reds -> red_kind -> reds
-
-(* Gives the constant list *)
-val red_get_const : reds -> bool * (evaluable_global_reference list)
 
 (*s Reduction function specification. *)
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5b602bfdc..272ecc57d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -93,57 +93,82 @@ let whd_flags flgs env sigma t =
 (*** Reduction using substitutions ***)
 (*************************************)
 
-(* Naive Implementation
-type flags = BETA | DELTA | EVAR | IOTA
-
-let red_beta = List.mem BETA
-let red_delta = List.mem DELTA
-let red_evar = List.mem EVAR
-let red_eta = List.mem ETA
-let red_iota = List.mem IOTA
-
-(* Local *)
-let beta = [BETA]
-let betaevar = [BETA;EVAR]
-let betaiota = [BETA;IOTA]
-
-(* Contextual *)
-let delta = [DELTA;EVAR]
-let betadelta = [BETA;DELTA;EVAR]
-let betadeltaeta = [BETA;DELTA;EVAR;ETA]
-let betadeltaiota = [BETA;DELTA;EVAR;IOTA]
-let betadeltaiotaeta = [BETA;DELTA;EVAR;IOTA;ETA]
-let betaiotaevar = [BETA;IOTA;EVAR]
-let betaeta = [BETA;ETA]
+(* This signature is very similar to Closure.RedFlagsSig except there
+   is eta but no per-constant unfolding *)
+
+module type RedFlagsSig = sig
+  type flags
+  type flag
+  val fbeta : flag
+  val fevar : flag
+  val fdelta : flag
+  val feta : flag
+  val fiota : flag
+  val fzeta : flag
+  val mkflags : flag list -> flags
+  val red_beta : flags -> bool
+  val red_delta : flags -> bool
+  val red_evar : flags -> bool
+  val red_eta : flags -> bool
+  val red_iota : flags -> bool
+  val red_zeta : flags -> bool
+end
+
+(* Naive Implementation 
+module RedFlags = (struct
+  type flag = BETA | DELTA | EVAR | IOTA | ZETA | ETA
+  type flags = flag list
+  let fbeta = BETA 
+  let fdelta = DELTA
+  let fevar = EVAR
+  let fiota = IOTA
+  let fzeta = ZETA
+  let feta = ETA
+  let mkflags l = l
+  let red_beta = List.mem BETA
+  let red_delta = List.mem DELTA
+  let red_evar = List.mem EVAR
+  let red_eta = List.mem ETA
+  let red_iota = List.mem IOTA
+  let red_zeta = List.mem ZETA
+end : RedFlagsSig)
 *)
 
 (* Compact Implementation *)
-type flags = int
-let fbeta = 1 and fdelta = 2 and fevar = 4 and feta = 8 and fiota = 16
-							and fletin = 32
-
-let red_beta f = f land fbeta <> 0
-let red_delta f = f land fdelta <> 0
-let red_evar f = f land fevar <> 0
-let red_eta f = f land feta <> 0
-let red_iota f = f land fiota <> 0
-let red_letin f = f land fletin <> 0
-
+module RedFlags = (struct
+  type flag = int
+  type flags = int
+  let fbeta = 1
+  let fdelta = 2
+  let fevar = 4
+  let feta = 8 
+  let fiota = 16
+  let fzeta = 32
+  let mkflags = List.fold_left (lor) 0
+  let red_beta f = f land fbeta <> 0
+  let red_delta f = f land fdelta <> 0
+  let red_evar f = f land fevar <> 0
+  let red_eta f = f land feta <> 0
+  let red_iota f = f land fiota <> 0
+  let red_zeta f = f land fzeta <> 0
+end : RedFlagsSig)
+
+open RedFlags
 
 (* Local *)
-let beta = fbeta
-let betaevar = fbeta lor fevar
-let betaiota = fbeta lor fiota
+let beta = mkflags [fbeta]
+let betaevar = mkflags [fevar; fbeta]
+let betaiota = mkflags [fiota; fbeta]
 
 (* Contextual *)
-let delta = fdelta lor fevar
-let betadelta = fbeta lor fdelta lor fletin lor fevar
-let betadeltaeta = fbeta lor fdelta lor fletin lor fevar lor feta
-let betadeltaiota = fbeta lor fdelta lor fletin lor fevar lor fiota
-let betadeltaiota_nolet = fbeta lor fdelta lor fevar lor fiota
-let betadeltaiotaeta = fbeta lor fdelta lor fletin lor fevar lor fiota lor feta
-let betaiotaevar = fbeta lor fiota lor fevar
-let betaetalet = fbeta lor feta lor fletin
+let delta = mkflags [fdelta;fevar]
+let betadelta = mkflags [fbeta;fdelta;fzeta;fevar]
+let betadeltaeta = mkflags [fbeta;fdelta;fzeta;fevar;feta]
+let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fevar;fiota]
+let betadeltaiota_nolet = mkflags [fbeta;fdelta;fevar;fiota]
+let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fevar;fiota;feta]
+let betaiotaevar = mkflags [fbeta;fiota;fevar]
+let betaetalet = mkflags [fbeta;feta;fzeta]
 
 (* Beta Reduction tools *)
 
@@ -216,6 +241,13 @@ let reduce_fix whdfun fix stack =
 
 (* Generic reduction function *)
 
+(* Y avait un commentaire pour whd_betadeltaiota :
+
+   NB : Cette fonction alloue peu c'est l'appel 
+     ``let (c,cargs) = whfun (recarg, empty_stack)''
+                              -------------------
+   qui coute cher *)
+
 let rec whd_state_gen flags env sigma = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
@@ -235,7 +267,7 @@ let rec whd_state_gen flags env sigma =
 	  (match constant_opt_value env const with
 	     | Some  body -> whrec (body, stack)
 	     | None -> s)
-      | IsLetIn (_,b,_,c) when red_letin flags -> stacklam whrec [b] c stack
+      | IsLetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
       | IsCast (c,_) -> whrec (c, stack)
       | IsApp (f,cl)  -> whrec (f, append_stack cl stack)
       | IsLambda (na,t,c) ->
@@ -280,7 +312,7 @@ let rec whd_state_gen flags env sigma =
 let local_whd_state_gen flags = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-      | IsLetIn (_,b,_,c) when red_letin flags -> stacklam whrec [b] c stack
+      | IsLetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
       | IsCast (c,_) -> whrec (c, stack)
       | IsApp (f,cl)  -> whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
@@ -321,21 +353,6 @@ let local_whd_state_gen flags =
   whrec
 
 (* 1. Beta Reduction Functions *)
-(*
-let whd_beta_state =
-  let rec whrec (x, stack as s) =
-    match kind_of_term x with
-      | IsLambda (name,c1,c2) ->
-	  (match decomp_stack stack with
-             | None -> (x,empty_stack)
-	     | Some (a1,rest) -> stacklam whrec [a1] c2 rest)
-
-      | IsCast (c,_) -> whrec (c, stack)
-      | IsApp (f,cl) -> whrec (f, append_stack cl stack)
-      | x -> s
-  in
-  whrec
-*)
 
 let whd_beta_state = local_whd_state_gen beta
 let whd_beta_stack x = appterm_of_stack (whd_beta_state (x, empty_stack))
@@ -349,119 +366,24 @@ let whd_betaetalet x = app_stack (whd_betaetalet_state (x,empty_stack))
 
 (* 2. Delta Reduction Functions *)
 
-(*
-let whd_delta_state env sigma = 
-  let rec whrec (x, l as s) =
-    match kind_of_term x with
-      | IsConst const when evaluable_constant env const ->
-	  whrec (constant_value env const, l)
-      | IsEvar (ev,args) when Evd.is_defined sigma ev ->
-          whrec (existential_value sigma (ev,args), l)
-      | IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
-      | IsCast (c,_) -> whrec (c, l)
-      | IsApp (f,cl) -> whrec (f, append_stack cl l)
-      | x -> s
-  in 
-  whrec
-*)
-
 let whd_delta_state e = whd_state_gen delta e
 let whd_delta_stack env sigma x =
   appterm_of_stack (whd_delta_state env sigma (x, empty_stack))
 let whd_delta env sigma c =
   app_stack (whd_delta_state env sigma (c, empty_stack))
 
-(*
-let whd_betadelta_state env sigma = 
-  let rec whrec (x, l as s) =
-    match kind_of_term x with
-      | IsConst const ->
-          if evaluable_constant env const then 
-	    whrec (constant_value env const, l)
-          else 
-	    s
-      | IsEvar (ev,args) ->
-          if Evd.is_defined sigma ev then 
-	    whrec (existential_value sigma (ev,args), l)
-          else 
-	    s
-      | IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
-      | IsCast (c,_) -> whrec (c, l)
-      | IsApp (f,cl)  -> whrec (f, append_stack cl l)
-      | IsLambda (_,_,c) ->
-          (match decomp_stack l with
-             | None -> s
-             | Some (a,m) -> stacklam whrec [a] c m)
-      | x -> s
-  in 
-  whrec
-*)
-
 let whd_betadelta_state e = whd_state_gen betadelta e
 let whd_betadelta_stack env sigma x =
   appterm_of_stack (whd_betadelta_state env sigma (x, empty_stack))
 let whd_betadelta env sigma c =
   app_stack (whd_betadelta_state env sigma (c, empty_stack))
 
-
-(*
-let whd_betaevar_stack env sigma = 
-  let rec whrec (x, l as s) =
-    match kind_of_term x with
-      | IsEvar (ev,args) ->
-          if Evd.is_defined sigma ev then 
-	    whrec (existential_value sigma (ev,args), l)
-          else 
-	    s
-      | IsCast (c,_) -> whrec (c, l)
-      | IsApp (f,cl)  -> whrec (f, append_stack cl l)
-      | IsLambda (_,_,c) ->
-          (match decomp_stack l with
-             | None -> s
-             | Some (a,m) -> stacklam whrec [a] c m)
-      | x -> s
-  in 
-  whrec
-*)
-
 let whd_betaevar_state e = whd_state_gen betaevar e
 let whd_betaevar_stack env sigma c =
   appterm_of_stack (whd_betaevar_state env sigma (c, empty_stack))
 let whd_betaevar env sigma c =
   app_stack (whd_betaevar_state env sigma (c, empty_stack))
 
-(*
-let whd_betadeltaeta_state env sigma = 
-  let rec whrec (x, l as s) =
-    match kind_of_term x with
-      | IsConst const when evaluable_constant env const ->
-	  whrec (constant_value env const, l)
-      | IsEvar (ev,args) when Evd.is_defined sigma ev ->
-	  whrec (existential_value sigma (ev,args), l)
-      | IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
-      | IsCast (c,_) -> whrec (c, l)
-      | IsApp (f,cl)  -> whrec (f, append_stack cl l)
-      | IsLambda (_,_,c) ->
-          (match decomp_stack l with
-             | None ->
-                 (match kind_of_term (app_stack (whrec (c, empty_stack))) with 
-                    | IsApp (f,cl) ->
-			let napp = Array.length cl in
-			if napp > 0 then
-			  let x',l' = whrec (array_last cl, empty_stack) in
-                          match kind_of_term x', decomp_stack l' with
-                            | IsRel 1, None ->
-				let lc = Array.sub cl 0 (napp - 1) in
-				let u = if napp=1 then f else appvect (f,lc) in
-				if noccurn 1 u then (pop u,empty_stack) else s
-                            | _ -> s
-			else s
-                    | _ -> s)
-             | Some (a,m) -> stacklam whrec [a] c m)
-      | x -> s
-  in 
-  whrec
-*)
 
 let whd_betadeltaeta_state e = whd_state_gen betadeltaeta e
 let whd_betadeltaeta_stack env sigma x =
@@ -471,166 +393,23 @@ let whd_betadeltaeta env sigma x =
 
 (* 3. Iota reduction Functions *)
 
-(* NB : Cette fonction alloue peu c'est l'appel 
-     ``let (recarg'hd,_ as recarg') = whfun recarg empty_stack in''
-                                     --------------------
-qui coute cher dans whd_betadeltaiota *)
-
-(*
-let whd_betaiota_state = 
-  let rec whrec (x,stack as s) =
-    match kind_of_term x with
-      | IsCast (c,_)     -> whrec (c, stack)
-      | IsApp (f,cl)    -> whrec (f, append_stack cl stack)
-      | IsLambda (_,_,c) ->
-          (match decomp_stack stack with
-             | None -> s
-             | Some (a,m) -> stacklam whrec [a] c m)
-      | IsMutCase (ci,p,d,lf) ->
-          let (c,cargs) = whrec (d, empty_stack) in
-          if reducible_mind_case c then
-            whrec (reduce_mind_case
-                     {mP=p; mconstr=c; mcargs=list_of_stack cargs;
-		      mci=ci; mlf=lf}, stack)
-          else 
-	    (mkMutCase (ci, p, app_stack (c,cargs), lf), stack)
-            
-      | IsFix fix ->
-	  (match reduce_fix whrec fix stack with
-             | Reduced s' -> whrec s'
-	     | NotReducible -> s)
-      | _ -> s
-  in 
-  whrec
-*)
-
 let whd_betaiota_state = local_whd_state_gen betaiota
 let whd_betaiota_stack x =
   appterm_of_stack (whd_betaiota_state (x, empty_stack))
 let whd_betaiota x =
   app_stack (whd_betaiota_state (x, empty_stack))
 
-(*
-let whd_betaiotaevar_state env sigma = 
-  let rec whrec (x, stack as s) =
-    match kind_of_term x with
-      | IsEvar (ev,args) ->
-          if Evd.is_defined sigma ev then 
-	    whrec (existential_value sigma (ev,args), stack)
-          else 
-	    s
-      | IsCast (c,_) -> whrec (c, stack)
-      | IsApp (f,cl)    -> whrec (f, append_stack cl stack)
-      | IsLambda (_,_,c) ->
-          (match decomp_stack stack with
-             | None -> s
-             | Some (a,m) -> stacklam whrec [a] c m)
-      | IsMutCase (ci,p,d,lf) ->
-          let (c,cargs) = whrec (d, empty_stack) in
-          if reducible_mind_case c then
-	    whrec (reduce_mind_case
-                     {mP=p; mconstr=c; mcargs=list_of_stack cargs;
-		      mci=ci; mlf=lf}, stack)
-          else 
-	    (mkMutCase (ci, p, app_stack (c,cargs), lf), stack)
-      | IsFix fix ->
-	  (match reduce_fix whrec fix stack with
-             | Reduced s' -> whrec s'
-	     | NotReducible -> s)
-      | _ -> s
- in 
-  whrec
-*)
-
 let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e
 let whd_betaiotaevar_stack env sigma x =
   appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
 let whd_betaiotaevar env sigma x = 
   app_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
 
-(*
-let whd_betadeltaiota_state env sigma =
-  let rec whrec (x, stack as s) =
-    match kind_of_term x with
-      | IsConst const when evaluable_constant env const ->
-	  whrec (constant_value env const, stack)
-      | IsEvar (ev,args) when Evd.is_defined sigma ev ->
-	  whrec (existential_value sigma (ev,args), stack)
-      | IsLetIn (_,b,_,c) -> stacklam whrec [b] c stack
-      | IsCast (c,_) -> whrec (c, stack)
-      | IsApp (f,cl)    -> whrec (f, append_stack cl stack)
-      | IsLambda (_,_,c) ->
-          (match decomp_stack stack with
-             | None -> s
-             | Some (a,m) -> stacklam whrec [a] c m)
-      | IsMutCase (ci,p,d,lf) ->
-          let (c,cargs) = whrec (d, empty_stack) in
-          if reducible_mind_case c then
-	    whrec (reduce_mind_case
-                     {mP=p; mconstr=c; mcargs=list_of_stack cargs;
-		      mci=ci; mlf=lf}, stack)
-          else 
-	    (mkMutCase (ci, p, app_stack (c,cargs), lf), stack)
-      | IsFix fix ->
-	  (match reduce_fix whrec fix stack with
-             | Reduced s' -> whrec s'
-	     | NotReducible -> s)
-      | _ -> s
-  in
-  whrec
-*)
-
 let whd_betadeltaiota_state e = whd_state_gen betadeltaiota e
 let whd_betadeltaiota_stack env sigma x =
   appterm_of_stack (whd_betadeltaiota_state env sigma (x, empty_stack))
 let whd_betadeltaiota env sigma x = 
   app_stack (whd_betadeltaiota_state env sigma (x, empty_stack))
-				
-(*				
-let whd_betadeltaiotaeta_state env sigma = 
-  let rec whrec (x, stack as s) =
-    match kind_of_term x with
-      | IsConst const when evaluable_constant env const ->
-	  whrec (constant_value env const, stack)
-      | IsEvar (ev,args) when Evd.is_defined sigma ev -> 
-	  whrec (existential_value sigma (ev,args), stack)
-      | IsLetIn (_,b,_,c) -> stacklam whrec [b] c stack
-      | IsCast (c,_) -> whrec (c, stack)
-      | IsApp (f,cl)    -> whrec (f, append_stack cl stack)
-      | IsLambda (_,_,c) ->
-          (match decomp_stack stack with
-             | None ->
-                 (match kind_of_term (app_stack (whrec (c, empty_stack))) with 
-                    | IsApp (f,cl) ->
-			let napp = Array.length cl in
-			if napp > 0 then
-			  let x', l' = whrec (array_last cl, empty_stack) in
-                          match kind_of_term x', decomp_stack l' with
-                            | IsRel 1, None ->
-				let lc = Array.sub cl 0 (napp-1) in
-				let u = if napp=1 then f else appvect (f,lc) in
-				if noccurn 1 u then (pop u,empty_stack) else s
-                            | _ -> s
-			else s
-                    | _ -> s)
-             | Some (a,m) -> stacklam whrec [a] c m)
-
-      | IsMutCase (ci,p,d,lf) ->
-          let (c,cargs) = whrec (d, empty_stack) in
-          if reducible_mind_case c then
-	    whrec (reduce_mind_case
-                     {mP=p; mconstr=c; mcargs=list_of_stack cargs;
-		      mci=ci; mlf=lf}, stack)
-          else 
-	    (mkMutCase (ci, p, app_stack (c,cargs), lf), stack)
-      | IsFix fix ->
-	  (match reduce_fix whrec fix stack with
-             | Reduced s' -> whrec s'
-	     | NotReducible -> s)
-      | _ -> s
-  in 
-  whrec
-*)
 
 let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
 let whd_betadeltaiotaeta_stack env sigma x =