diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/names.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 4 | ||||
| -rw-r--r-- | kernel/reduction.mli | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f60e2dbe0f..ac4efc515d 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -653,7 +653,7 @@ let check_one_fix renv recpos def = (* if [t] does not make recursive calls, it is guarded: *) if noccur_with_meta renv.rel_min nfi t then () else - let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in + let (f,l) = decompose_app (whd_betaiotazeta t) in match kind_of_term f with | Rel p -> (* Test if [p] is a fixpoint (recursive call) *) diff --git a/kernel/names.ml b/kernel/names.ml index 38eb38beaf..d1c6ee8a44 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -65,7 +65,7 @@ let repr_dirpath x = x let empty_dirpath = [] let string_of_dirpath = function - | [] -> "_empty_" + | [] -> "<>" | sl -> String.concat "." (List.map string_of_id (List.rev sl)) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 7a6c560f81..ba7e8c41d7 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -90,11 +90,11 @@ let pure_stack lfts stk = let nf_betaiota t = norm_val (create_clos_infos betaiota empty_env) (inject t) -let whd_betaiotazeta env x = +let whd_betaiotazeta x = match kind_of_term x with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> x - | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x) let whd_betadeltaiota env t = match kind_of_term t with diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 663c18e2cc..2e344b2178 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -17,7 +17,7 @@ open Closure (************************************************************************) (*s Reduction functions *) -val whd_betaiotazeta : env -> constr -> constr +val whd_betaiotazeta : constr -> constr val whd_betadeltaiota : env -> constr -> constr val whd_betadeltaiota_nolet : env -> constr -> constr |