From e9be775a92869a371d229c9bfebcd0c7270122b7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Jul 2014 19:03:29 +0200
Subject: More straightforward definition of Universes.add_list_map.

---
 library/universes.ml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/library/universes.ml b/library/universes.ml
index 788af000ba..c38d25d759 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -475,14 +475,12 @@ let new_global_univ () =
 
 module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap)
 
-let add_list_map u t map = 
-  let l, d, r = LMap.split u map in
-  let d' = match d with None -> [t] | Some l -> t :: l in
-  let lr = 
-    LMap.merge (fun k lm rm -> 
-      match lm with Some t -> lm | None ->
-      match rm with Some t -> rm | None -> None) l r
-  in LMap.add u d' lr
+let add_list_map u t map =
+  try
+    let l = LMap.find u map in
+    LMap.update u (t :: l) map
+  with Not_found ->
+    LMap.add u [t] map
 
 module UF = LevelUnionFind
 
-- 
cgit v1.2.3