diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 19:03:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 19:03:29 +0200 |
| commit | e9be775a92869a371d229c9bfebcd0c7270122b7 (patch) | |
| tree | 503c93883bef786ed181c9470d066e882f747710 /library | |
| parent | 2b7ccb235b503f4c978009c2d7908d305cf85925 (diff) | |
More straightforward definition of Universes.add_list_map.
Diffstat (limited to 'library')
| -rw-r--r-- | library/universes.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/library/universes.ml b/library/universes.ml index 788af000b..c38d25d75 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 |