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

9 files changed, 289 insertions, 359 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 2b0f93b0e3..0000b26a18 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -101,7 +101,8 @@ let none = Evd.empty
 
 let type_of env c = Typing.type_of env Evd.empty (strip_outer_cast c)
 
-let whd_betaiotalet = clos_norm_flags (UNIFORM, red_add betaiota_red ZETA)
+open RedFlags
+let whd_betaiotalet = clos_norm_flags (UNIFORM, mkflags [fBETA;fIOTA;fZETA])
 
 let is_axiom sp = (Global.lookup_constant sp).const_body = None
 
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index a326a7a18c..0a70426ea5 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -548,13 +548,15 @@ let constants_to_unfold =
 (*    SectionPathSet.empty *)
 
 (* Unfolds the functions interp and find_btree in the term c of goal gl *)
+open RedFlags
 let polynom_unfold_tac =
-  let flags = (UNIFORM, red_add betaiota_red (CONST constants_to_unfold)) in
+  let flags =
+    (UNIFORM, mkflags(fBETA::fIOTA::fEVAR::(List.map fCONST constants_to_unfold))) in
   reduct_in_concl (cbv_norm_flags flags)
       
 let polynom_unfold_tac_in_term gl =
   let flags = 
-    (UNIFORM, red_add betaiotazeta_red (CONST constants_to_unfold)) 
+    (UNIFORM,mkflags(fBETA::fIOTA::fEVAR::fZETA::(List.map fCONST constants_to_unfold)))
   in
   cbv_norm_flags flags (pf_env gl) (project gl)
 
diff --git a/kernel/closure.ml b/kernel/closure.ml
index a09368fcdc..81c1b7bcca 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 e401679181..6f5afc4e27 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 5b602bfdcc..272ecc57d7 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 =
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index b864d10314..e29fab4e26 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -136,11 +136,13 @@ let red_allowed flags stack rk =
   else 
     red_top flags rk
 
+open RedFlags
+
 let red_allowed_ref flags stack = function
-  | FarRelBinding _ -> red_allowed flags stack DELTA
-  | VarBinding id -> red_allowed flags stack (VAR id)
-  | EvarBinding _ -> red_allowed flags stack EVAR
-  | ConstBinding (sp,_) -> red_allowed flags stack (CONST [sp])
+  | FarRelBinding _ -> red_allowed flags stack fDELTA
+  | VarBinding id -> red_allowed flags stack (fVAR id)
+  | EvarBinding _ -> red_allowed flags stack fEVAR
+  | ConstBinding (sp,_) -> red_allowed flags stack (fCONST sp)
 
 (* Transfer application lists from a value to the stack
  * useful because fixpoints may be totally applied in several times
@@ -173,7 +175,7 @@ let rec check_app_constr redfun = function
   | (_::l, n) -> check_app_constr redfun (l,(pred n))
 	
 let fixp_reducible redfun flgs ((reci,i),_) stk =
-  if red_allowed flgs stk IOTA then
+  if red_allowed flgs stk fIOTA then
     match stk with               (* !!! for Acc_rec: reci.(i) = -2 *)
       | APP(appl,_) -> reci.(i) >=0 & check_app_constr redfun (appl, reci.(i))
       | _ -> false
@@ -181,7 +183,7 @@ let fixp_reducible redfun flgs ((reci,i),_) stk =
     false
 
 let cofixp_reducible redfun flgs _ stk =
-  if red_allowed flgs stk IOTA then
+  if red_allowed flgs stk fIOTA then
     match stk with
       | (CASE _ | APP(_,CASE _)) -> true
       | _ -> false
@@ -239,9 +241,9 @@ let rec norm_head info env t stack =
   | IsLetIn (x, b, t, c) ->
       (* zeta means letin are contracted; delta without zeta means we *)
       (* allow substitution but leave let's in place *)
-      let zeta = red_allowed (info_flags info) stack ZETA in
+      let zeta = red_allowed (info_flags info) stack fZETA in
       let env' =
-	if zeta or red_allowed (info_flags info) stack DELTA then 
+	if zeta or red_allowed (info_flags info) stack fDELTA then 
 	  subs_cons (cbv_stack_term info TOP env b,env)
 	else
 	  subs_lift env in
@@ -295,7 +297,7 @@ and cbv_stack_term info stack env t =
   match norm_head info env t stack with
     (* a lambda meets an application -> BETA *)
     | (LAM (x,a,b,env), APP (arg::args, stk))
-      when red_allowed (info_flags info) stk BETA ->
+      when red_allowed (info_flags info) stk fBETA ->
         let subs = subs_cons (arg,env) in
           cbv_stack_term info (stack_app args stk) subs b
 
@@ -314,14 +316,14 @@ and cbv_stack_term info stack env t =
     (* constructor in a Case -> IOTA
        (use red_under because we know there is a Case) *)
     | (CONSTR(n,sp,_,_), APP(args,CASE(_,br,(arity,_),env,stk)))
-            when red_under (info_flags info) IOTA ->
+            when red_under (info_flags info) fIOTA ->
 	let ncargs = arity.(n-1) in
 	let real_args = list_lastn ncargs args in
         cbv_stack_term info (stack_app real_args stk) env br.(n-1)
          
     (* constructor of arity 0 in a Case -> IOTA ( "   " )*)
     | (CONSTR(n,_,_,_), CASE(_,br,_,env,stk))
-                  when red_under (info_flags info) IOTA ->
+                  when red_under (info_flags info) fIOTA ->
                     cbv_stack_term info stk env br.(n-1)
 
     (* may be reduced later by application *)  
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 778eebff76..7271a3c0be 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -46,6 +46,7 @@ val stack_app : cbv_value list -> cbv_stack -> cbv_stack
 val under_case_stack : cbv_stack -> bool
 val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
 
+open RedFlags
 val red_allowed : flags -> cbv_stack -> red_kind -> bool
 val reduce_const_body :
   (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 45fe9e5a47..8bfa53842c 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -354,8 +354,10 @@ let rec ast_of_cvt_intro_pattern = function
   | ListPat l -> ope ("LISTPATTERN",  (List.map ast_of_cvt_intro_pattern l))
 
 (* Gives the ast list corresponding to a reduction flag *)
+open RedFlags
+
 let last_of_cvt_flags (_,red) =
-  (if (red_set red BETA) then [ope("Beta",[])]
+  (if (red_set red fBETA) then [ope("Beta",[])]
    else [])@
   (let (n_unf,lconst) = red_get_const red in
    let lqid =
@@ -368,7 +370,7 @@ let last_of_cvt_flags (_,red) =
    if lqid = [] then []
    else if n_unf then [ope("Delta",[]);ope("UnfBut",lqid)]
    else [ope("Delta",[]);ope("Unf",lqid)])@
-  (if (red_set red IOTA) then [ope("Iota",[])]
+  (if (red_set red fIOTA) then [ope("Iota",[])]
    else [])
 
 (* Gives the ast corresponding to a reduction expression *)
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index cb53954471..90bb5d805b 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -10,6 +10,7 @@
 
 open Astterm
 open Closure
+open RedFlags
 open Declarations
 open Dyn
 open Libobject
@@ -1110,7 +1111,7 @@ and cvt_fold (evc,env,lfun,lmatch,goalopt,debug) = function
 and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf =
   let rec add_flag red = function
     | [] -> red
-    | Node(_,"Beta",[])::lf -> add_flag (red_add red BETA) lf
+    | Node(_,"Beta",[])::lf -> add_flag (red_add red fBETA) lf
     | Node(_,"Delta",[])::lf ->
 	(match lf with
 	   | Node(loc,"Unf",l)::lf ->
@@ -1119,8 +1120,8 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf =
 		   (fun v red -> 
 		      match glob_const_nvar loc env
                         (qid_interp (evc,env,lfun,lmatch,goalopt,debug) v) with
-			| EvalVarRef id -> red_add red (VAR id)
-			| EvalConstRef sp -> red_add red (CONST [sp])) l red
+			| EvalVarRef id -> red_add red (fVAR id)
+			| EvalConstRef sp -> red_add red (fCONST sp)) l red
 	       in add_flag idl lf
 (*
 (id_of_Identifier (unvarg
@@ -1133,18 +1134,12 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf =
 		   (fun v red -> 
 		      match glob_const_nvar loc env
                         (qid_interp (evc,env,lfun,lmatch,goalopt,debug)v) with
-			| EvalVarRef id -> red_add red (VARBUT id)
-			| EvalConstRef sp -> red_add red (CONSTBUT [sp])) l red
+			| EvalVarRef id -> red_add red (fVARBUT id)
+			| EvalConstRef sp -> red_add red (fCONSTBUT sp)) l red
 	       in add_flag idl lf
 
-(*
-		 List.map
-		   (fun v -> glob_const_nvar loc (id_of_Identifier (unvarg
-                   (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l
-               in add_flag (red_add red (CONSTBUT idl)) lf
-*)
-	   | _ -> add_flag (red_add red DELTA) lf)
-    | Node(_,"Iota",[])::lf -> add_flag (red_add red IOTA) lf
+	   | _ -> add_flag (red_add red fDELTA) lf)
+    | Node(_,"Iota",[])::lf -> add_flag (red_add red fIOTA) lf
     | Node(loc,("Unf"|"UnfBut"),l)::_ ->
 	user_err_loc(loc,"flag_of_ast",
                      [<'sTR "Delta must be specified just before">])