From d846451c9a07b4e051173878a5446edea029bf5b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 18 Nov 2014 11:02:17 +0100
Subject: Making map_union a standard function of the ML library.

---
 pretyping/miscops.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 3e5f7577bf..882ebafe11 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)
-- 
cgit v1.2.3