diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-18 12:04:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-18 15:10:23 +0200 |
| commit | 77839ae306380e99a8ceac0bf26ff86ec9159346 (patch) | |
| tree | fb2634db286be45a23a57a990e05eed8e9e6597e /kernel/univ.ml | |
| parent | 4c79604793ddf9c3e717d762518200b5e7db4f35 (diff) | |
Code factorization in LMap.
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 17 |
1 files changed, 1 insertions, 16 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 83d86ea24..7c9a5ca32 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -415,24 +415,9 @@ module LMap = struct else add u v acc) ext empty - let elements = bindings - let of_set s d = - LSet.fold (fun u -> add u d) s - empty - - let of_list l = - List.fold_left (fun m (u, v) -> add u v m) empty l - - let universes m = - fold (fun u _ acc -> LSet.add u acc) m LSet.empty - let pr f m = h 0 (prlist_with_sep fnl (fun (u, v) -> - Level.pr u ++ f v) (elements m)) - - let find_opt t m = - try Some (find t m) - with Not_found -> None + Level.pr u ++ f v) (bindings m)) end type 'a universe_map = 'a LMap.t |