diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 25 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 2 |
2 files changed, 25 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 0d7f77edae..cd975ee9a9 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) (********************************************************************) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f43b01d1bb..eeb9c421a1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -223,7 +223,7 @@ let rec unzip ctx j = let feedback_completion_typecheck = let open Feedback in Option.iter (fun state_id -> - feedback ~id:(State state_id) Feedback.Complete) + feedback ~id:state_id Feedback.Complete) let infer_declaration ~trust env kn dcl = match dcl with |