From 485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 15:23:15 +0200
Subject: Use type Universes.universe_binders.

---
 engine/evd.mli    |  2 +-
 engine/uState.ml  | 24 ++++++++++--------------
 engine/uState.mli |  2 +-
 3 files changed, 12 insertions(+), 16 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.mli b/engine/evd.mli
index 17fa150454..853a34bc43 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 01a4798217..123b64314c 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 1c906fcb2d..f54bcc832a 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
-- 
cgit v1.2.3