aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/miscops.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 3e5f7577b..882ebafe1 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -46,10 +46,6 @@ let map_flags f flags =
let map_occs f (occ,e) = (occ,f e)
-let map_union f g = function
- | Inl a -> Inl (f a)
- | Inr b -> Inr (g b)
-
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)