diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 3 | ||||
| -rw-r--r-- | kernel/reduction.mli | 1 |
3 files changed, 5 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index e5d73b6e2a..343fae48a3 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -344,7 +344,7 @@ let build_branches_type ind (_,mip as specif) params p = (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) let build_case_type n p c realargs = - betazeta_appvect (n+1) p (Array.of_list (realargs@[c])) + whd_betaiota (betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) let type_case_branches env (ind,largs) pj c = let specif = lookup_mind_specif env ind in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index e215f23361..e8fea82800 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -94,6 +94,9 @@ let pure_stack lfts stk = (* Reduction Functions *) (****************************************************************************) +let whd_betaiota t = + whd_val (create_clos_infos betaiota empty_env) (inject t) + let nf_betaiota t = norm_val (create_clos_infos betaiota empty_env) (inject t) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index a6ebda4918..ced0fd3413 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -17,6 +17,7 @@ val whd_betaiotazeta : constr -> constr val whd_betadeltaiota : env -> constr -> constr val whd_betadeltaiota_nolet : env -> constr -> constr +val whd_betaiota : constr -> constr val nf_betaiota : constr -> constr (*********************************************************************** |