Code factorization in LMap.

3 files changed, 3 insertions, 36 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
diff --git a/kernel/univ.mli b/kernel/univ.mli
index a76cf9ea8..832da157e 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -232,7 +232,7 @@ val univ_depends : universe -> universe -> bool
 (** Polymorphic maps from universe levels to 'a *)
 module LMap : 
 sig
-  include Map.S with type key = universe_level
+  include CMap.ExtS with type key = universe_level and module Set := LSet
 
   val union : 'a t -> 'a t -> 'a t
   (** [union x y] favors the bindings in the first map. *)
@@ -244,24 +244,6 @@ sig
   (** [subst_union x y] favors the bindings of the first map that are [Some],
       otherwise takes y's bindings. *)
 
-  val elements : 'a t -> (universe_level * 'a) list
-  (** As an association list *)
-
-  val of_list : (universe_level * 'a) list -> 'a t
-  (** From an association list *)
-
-  val of_set : universe_set -> 'a -> 'a t
-  (** Associates the same value to all levels in the set *)
-
-  val mem : universe_level -> 'a t -> bool
-  (** Is there a binding for the level? *)
-
-  val find_opt : universe_level -> 'a t -> 'a option
-  (** Find the value associated to the level, if any *)
-
-  val universes : 'a t -> universe_set
-  (** The domain of the map *)
-
   val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
   (** Pretty-printing *)
 end
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 53d1a8a0e..8b9631b4b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -966,7 +966,7 @@ let merge_uctx rigid uctx ctx' =
     | UnivRigid -> uctx
     | UnivFlexible b ->
       let uvars' = Univ.LMap.subst_union uctx.uctx_univ_variables 
-	(Univ.LMap.of_set (Univ.ContextSet.levels ctx') None) in
+	(Univ.LMap.bind (fun _ -> None) (Univ.ContextSet.levels ctx')) in
 	if b then
 	  { uctx with uctx_univ_variables = uvars';
 	  uctx_univ_algebraic = Univ.LSet.union uctx.uctx_univ_algebraic