diff options
| -rw-r--r-- | kernel/reduction.ml | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 0d7f77eda..cd975ee9a 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -107,7 +107,15 @@ let pure_stack lfts stk = (****************************************************************************) let whd_betaiota env t = - whd_val (create_clos_infos betaiota env) (inject t) + match kind_of_term t with + | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| + Prod _|Lambda _|Fix _|CoFix _) -> t + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t + | _ -> whd_val (create_clos_infos betaiota env) (inject t) + end + | _ -> whd_val (create_clos_infos betaiota env) (inject t) let nf_betaiota env t = norm_val (create_clos_infos betaiota env) (inject t) @@ -116,18 +124,33 @@ let whd_betaiotazeta env x = match kind_of_term x with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> x + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x + | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + end | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) let whd_all env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ -> t + | _ -> whd_val (create_clos_infos all env) (inject t) + end | _ -> whd_val (create_clos_infos all env) (inject t) let whd_allnolet env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t + | _ -> whd_val (create_clos_infos allnolet env) (inject t) + end | _ -> whd_val (create_clos_infos allnolet env) (inject t) (********************************************************************) |