diff options
| author | Pierre-Marie Pédrot | 2021-01-06 16:08:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-18 13:36:46 +0100 |
| commit | 5dcf8f4d0fb7419c07b9287db22f6ed6cbf000a4 (patch) | |
| tree | 35fdde54ab660c1c0e3dff0de8ce00fd87e8832e /pretyping/reductionops.ml | |
| parent | 5b08cdcd4bde7fdcd21f7a0f0912f0021847294b (diff) | |
Move the only use of strong_with_flags to its single calling module.
This also allows to move the strong variant of cbn to the Cbn module.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 12 |
1 files changed, 0 insertions, 12 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 |