Separate checking univ_decls and obtaining universe binder names.

4 files changed, 15 insertions, 8 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index ca1196b948..67ae73ceb2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -936,6 +936,8 @@ let universe_of_name evd s = UState.universe_of_name evd.universes s
 let add_universe_name evd s l =
   { evd with universes = UState.add_universe_name evd.universes s l }
 
+let universe_binders evd = UState.universe_binders evd.universes
+
 let universes evd = UState.ugraph evd.universes
 
 let update_sigma_env evd env =
diff --git a/engine/evd.mli b/engine/evd.mli
index 36c399e986..b6157202de 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -509,7 +509,8 @@ val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 val add_universe_name : evar_map -> Id.t -> Univ.Level.t -> evar_map
 
-val add_constraints_context : UState.t -> 
+val universe_binders : evar_map -> Universes.universe_binders
+val add_constraints_context : UState.t ->
   Univ.constraints -> UState.t
 
 
@@ -552,12 +553,12 @@ 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 ->
-  Universes.universe_binders * Univ.UContext.t
+  Univ.UContext.t
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
 val check_univ_decl : evar_map -> UState.universe_decl ->
-  Universes.universe_binders * Univ.UContext.t
+  Univ.UContext.t
 
 val merge_universe_context : evar_map -> UState.t -> evar_map
 val set_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index 498d73fd37..282acb3d6e 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -114,6 +114,8 @@ let of_binders b =
   in
   { ctx with uctx_names = b, rmap }
 
+let universe_binders ctx = fst ctx.uctx_names
+
 let instantiate_variable l b v =
   try v := Univ.LMap.update l (Some b) !v
   with Not_found -> assert false
@@ -291,7 +293,7 @@ let universe_context ~names ~extensible uctx =
     let inst = Univ.Instance.of_array inst in
     let ctx = Univ.UContext.make (inst,
                                   Univ.ContextSet.constraints uctx.uctx_local) in
-    fst uctx.uctx_names, ctx
+    ctx
 
 let check_implication uctx cstrs ctx =
   let gr = initial_graph uctx in
@@ -303,14 +305,14 @@ let check_implication uctx cstrs ctx =
 
 let check_univ_decl uctx decl =
   let open Misctypes in
-  let pl, ctx = universe_context
+  let ctx = universe_context
       ~names:decl.univdecl_instance
       ~extensible:decl.univdecl_extensible_instance
       uctx
   in
   if not decl.univdecl_extensible_constraints then
     check_implication uctx decl.univdecl_constraints ctx;
-  pl, ctx
+  ctx
 
 let restrict ctx vars =
   let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
diff --git a/engine/uState.mli b/engine/uState.mli
index 7f2357a685..38af08f910 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -32,6 +32,8 @@ val of_context_set : Univ.ContextSet.t -> t
 
 val of_binders : Universes.universe_binders -> t
 
+val universe_binders : t -> Universes.universe_binders
+
 (** {5 Projections} *)
 
 val context_set : t -> Univ.ContextSet.t
@@ -135,12 +137,12 @@ 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 ->
-  Universes.universe_binders * Univ.UContext.t
+  Univ.UContext.t
 
 type universe_decl =
   (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
 
-val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.UContext.t
+val check_univ_decl : t -> universe_decl -> Univ.UContext.t
 
 (** {5 TODO: Document me} *)