diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 12 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 3 |
2 files changed, 0 insertions, 15 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3da75f67b9..d52be18faa 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -468,18 +468,6 @@ let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) with Not_found -> None -let strong_with_flags whdfun flags env sigma t = - let push_rel_check_zeta d env = - let open CClosure.RedFlags in - let d = match d with - | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t) - | d -> d in - push_rel d env in - let rec strongrec env t = - map_constr_with_full_binders env sigma - push_rel_check_zeta strongrec env (whdfun flags env sigma t) in - strongrec env t - let strong whdfun env sigma t = let rec strongrec env t = map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 59bc4a8b72..93cb4c190c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -145,9 +145,6 @@ type stack_reduction_function = (** {6 Reduction Function Operators } *) -val strong_with_flags : - (CClosure.RedFlags.reds -> reduction_function) -> - (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function (** {6 Generic Optimized Reduction Function using Closures } *) |