Use type Universes.universe_binders.

5 files changed, 14 insertions, 18 deletions

diff --git a/API/API.mli b/API/API.mli
index 1f1b05ead..d912dc771 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2882,7 +2882,7 @@ sig
     val evar_ident : evar -> evar_map -> Names.Id.t option
     val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
     val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map ->
-                           (Names.Id.t * Univ.Level.t) list * Univ.UContext.t
+                           Universes.universe_binders * Univ.UContext.t
     val nf_constraints : evar_map -> evar_map
     val from_ctx : UState.t -> evar_map
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 17fa15045..853a34bc4 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -552,7 +552,7 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
 val evar_universe_context : evar_map -> UState.t
 val universe_context_set : evar_map -> Univ.ContextSet.t
 val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map ->
-		       (Id.t * Univ.Level.t) list * Univ.UContext.t
+  Universes.universe_binders * Univ.UContext.t
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 01a479821..123b64314 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -11,20 +11,8 @@ open CErrors
 open Util
 open Names
 
-module StringOrd = struct type t = string let compare = String.compare end
-module UNameMap = struct
+module UNameMap = String.Map
     
-  include Map.Make(StringOrd)
-    
-  let union s t = 
-    if s == t then s
-    else
-      merge (fun k l r -> 
-        match l, r with
-        | Some _, _ -> l
-        | _, _ -> r) s t
-end
-
 type uinfo = {
   uname : string option;
   uloc : Loc.t option;
@@ -59,12 +47,20 @@ let is_empty ctx =
   Univ.ContextSet.is_empty ctx.uctx_local && 
     Univ.LMap.is_empty ctx.uctx_univ_variables
 
+let uname_union s t =
+  if s == t then s
+  else
+    UNameMap.merge (fun k l r ->
+        match l, r with
+        | Some _, _ -> l
+        | _, _ -> r) s t
+
 let union ctx ctx' =
   if ctx == ctx' then ctx
   else if is_empty ctx' then ctx
   else
     let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
-    let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
+    let names = uname_union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
     let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
                                (Univ.ContextSet.levels ctx.uctx_local) in
     let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
diff --git a/engine/uState.mli b/engine/uState.mli
index 1c906fcb2..f54bcc832 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -135,7 +135,7 @@ val normalize : t -> t
     Also return the association list of universe names and universes
     (including those not in [names]). *)
 val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t ->
-  (Id.t * Univ.Level.t) list * Univ.UContext.t
+  Universes.universe_binders * Univ.UContext.t
 
 type universe_decl =
   (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
diff --git a/interp/declare.ml b/interp/declare.ml
index 1a589897b..7ab13b859 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -457,7 +457,7 @@ let declare_universe_context poly ctx =
   Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
 
 (* Discharged or not *)
-type universe_decl = polymorphic * (Id.t * Univ.Level.t) list
+type universe_decl = polymorphic * Universes.universe_binders
 
 let cache_universes (p, l) =
   let glob = Global.global_universe_names () in