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

1 files changed, 9 insertions, 9 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 710bfa19b8..2dc2f0c7c9 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -107,17 +107,17 @@ let whd_betaiotazeta env x =
        Prod _|Lambda _|Fix _|CoFix _) -> x
     | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
 
-let whd_betadeltaiota env t =
+let whd_all env t =
   match kind_of_term t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> t
-    | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t)
+    | _ -> whd_val (create_clos_infos all env) (inject t)
 
-let whd_betadeltaiota_nolet env t =
+let whd_allnolet env t =
   match kind_of_term t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
-    | _ -> whd_val (create_clos_infos betadeltaiotanolet env) (inject t)
+    | _ -> whd_val (create_clos_infos allnolet env) (inject t)
 
 (********************************************************************)
 (*                         Conversion                               *)
@@ -731,7 +731,7 @@ let betazeta_appvect = lambda_appvect_assum
  * error message. *)
 
 let hnf_prod_app env t n =
-  match kind_of_term (whd_betadeltaiota env t) with
+  match kind_of_term (whd_all env t) with
     | Prod (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
 
@@ -742,7 +742,7 @@ let hnf_prod_applist env t nl =
 
 let dest_prod env =
   let rec decrec env m c =
-    let t = whd_betadeltaiota env c in
+    let t = whd_all env c in
     match kind_of_term t with
       | Prod (n,a,c0) ->
 	  let d = LocalAssum (n,a) in
@@ -754,7 +754,7 @@ let dest_prod env =
 (* The same but preserving lets in the context, not internal ones. *)
 let dest_prod_assum env =
   let rec prodec_rec env l ty =
-    let rty = whd_betadeltaiota_nolet env ty in
+    let rty = whd_allnolet env ty in
     match kind_of_term rty with
     | Prod (x,t,c)  ->
         let d = LocalAssum (x,t) in
@@ -764,7 +764,7 @@ let dest_prod_assum env =
 	prodec_rec (push_rel d env) (Context.Rel.add d l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               ->
-      let rty' = whd_betadeltaiota env rty in
+      let rty' = whd_all env rty in
 	if Term.eq_constr rty' rty then l, rty
 	else prodec_rec env l rty'
   in
@@ -772,7 +772,7 @@ let dest_prod_assum env =
 
 let dest_lam_assum env =
   let rec lamec_rec env l ty =
-    let rty = whd_betadeltaiota_nolet env ty in
+    let rty = whd_allnolet env ty in
     match kind_of_term rty with
     | Lambda (x,t,c)  ->
         let d = LocalAssum (x,t) in