diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 710bfa19b..2dc2f0c7c 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 |