diff options
Diffstat (limited to 'pretyping/miscops.ml')
| -rw-r--r-- | pretyping/miscops.ml | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 1b536bfda..1697e54ab 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -10,7 +10,6 @@ open Util open Misctypes -open Genredexpr (** Mapping [cast_type] *) @@ -42,26 +41,6 @@ let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with | IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2 | _ -> false -(** Mapping [red_expr_gen] *) - -let map_flags f flags = - { flags with rConst = List.map f flags.rConst } - -let map_occs f (occ,e) = (occ,f e) - -let map_red_expr_gen f g h = function - | Fold l -> Fold (List.map f l) - | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l) - | Simpl (flags,occs_o) -> - Simpl (map_flags g flags, Option.map (map_occs (map_union g h)) occs_o) - | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l) - | Cbv flags -> Cbv (map_flags g flags) - | Lazy flags -> Lazy (map_flags g flags) - | CbvVm occs_o -> CbvVm (Option.map (map_occs (map_union g h)) occs_o) - | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o) - | Cbn flags -> Cbn (map_flags g flags) - | ExtraRedExpr _ | Red _ | Hnf as x -> x - (** Mapping bindings *) let map_explicit_bindings f l = |