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

5 files changed, 12 insertions, 10 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 853410db8b..ef38458578 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -72,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 exception NotExtensibleClause
 
 let clenv_push_prod cl =
-  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
   let rec clrec typ = match kind_of_term typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
diff --git a/proofs/logic.ml b/proofs/logic.ml
index fd8a70c650..bfaeae712c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -463,7 +463,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
 and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
-    let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in
+    let t = whd_all (Goal.V82.env sigma goal) sigma funty in
     let rec collapse t = match kind_of_term t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
     | _ -> t
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index ee55915211..d5e3f30af3 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -146,7 +146,9 @@ let make_flag_constant = function
 let make_flag env f =
   let red = no_red in
   let red = if f.rBeta then red_add red fBETA else red in
-  let red = if f.rIota then red_add red fIOTA else red in
+  let red = if f.rMatch then red_add red fMATCH else red in
+  let red = if f.rFix then red_add red fFIX else red in
+  let red = if f.rCofix then red_add red fCOFIX else red in
   let red = if f.rZeta then red_add red fZETA else red in
   let red =
     if f.rDelta then (* All but rConst *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8c0b4ba98a..50984c48e0 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -84,7 +84,7 @@ let pf_eapply f gls x =
 let pf_reduce = pf_apply
 let pf_e_reduce = pf_apply
 
-let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
+let pf_whd_all         = pf_reduce whd_all
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_nf                        = pf_reduce simpl
 let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
@@ -101,7 +101,7 @@ let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let pf_hnf_type_of gls          = pf_whd_betadeltaiota gls % pf_get_type_of gls
+let pf_hnf_type_of gls          = pf_whd_all gls % pf_get_type_of gls
 
 let pf_is_matching              = pf_apply Constr_matching.is_matching_conv
 let pf_matches                  = pf_apply Constr_matching.matches_conv
@@ -219,7 +219,7 @@ module New = struct
     let sigma = project gl in
     nf_evar sigma concl
 
-  let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+  let pf_whd_all gl t = pf_apply whd_all gl t
 
   let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
 
@@ -228,11 +228,11 @@ module New = struct
 
   let pf_hnf_constr gl t = pf_apply hnf_constr gl t
   let pf_hnf_type_of gl t =
-    pf_whd_betadeltaiota gl (pf_get_type_of gl t)
+    pf_whd_all gl (pf_get_type_of gl t)
 
   let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
 
-  let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+  let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
   let pf_nf_evar gl t = nf_evar (project gl) t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 182433cb3a..100ed1522e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -63,7 +63,7 @@ val pf_e_reduce :
   (env -> evar_map -> constr -> evar_map * constr) ->
   goal sigma -> constr -> evar_map * constr
 
-val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
+val pf_whd_all       : goal sigma -> constr -> constr
 val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
 val pf_nf_betaiota             : goal sigma -> constr -> constr
@@ -127,7 +127,7 @@ module New : sig
   val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
   val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
 
-  val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
   val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
 
   val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map