Stop exposing UState.universe_context and its Evd wrapper.

We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).

3 files changed, 17 insertions, 18 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 67ae73ceb2..eb0f2e3e74 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -756,8 +756,7 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = UState.context_set d.universes
 
-let universe_context ~names ~extensible evd =
-  UState.universe_context ~names ~extensible evd.universes
+let to_universe_context evd = UState.context evd.universes
 
 let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl
 
diff --git a/engine/evd.mli b/engine/evd.mli
index b6157202de..49b6a75833 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -492,6 +492,8 @@ type 'a in_evar_universe_context = 'a * UState.t
 val evar_universe_context_set : UState.t -> Univ.ContextSet.t
 val evar_universe_context_constraints : UState.t -> Univ.constraints
 val evar_context_universe_context : UState.t -> Univ.UContext.t
+[@@ocaml.deprecated "alias of UState.context"]
+
 val evar_universe_context_of : Univ.ContextSet.t -> UState.t
 val empty_evar_universe_context : UState.t
 val union_evar_universe_context : UState.t -> UState.t ->
@@ -552,11 +554,14 @@ 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 ->
-  Univ.UContext.t
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
+(** [to_universe_context evm] extracts the local universes and
+    constraints of [evm] and orders the universes the same as
+    [Univ.ContextSet.to_context]. *)
+val to_universe_context : evar_map -> Univ.UContext.t
+
 val check_univ_decl : evar_map -> UState.universe_decl ->
   Univ.UContext.t
 
diff --git a/engine/uState.mli b/engine/uState.mli
index 38af08f910..5279c63884 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -125,23 +125,18 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
 val normalize : t -> t
 
-(** [universe_context names extensible ctx]
-
-    Return a universe context containing the local universes of [ctx]
-    and their constraints. The universes corresponding to [names] come
-    first in the order defined by that list.
-
-    If [extensible] is false, check that the universes of [names] are
-    the only local universes.
-
-    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 ->
-  Univ.UContext.t
-
 type universe_decl =
   (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
 
+(** [check_univ_decl ctx decl]
+
+   If non extensible in [decl], check that the local universes (resp.
+   universe constraints) in [ctx] are implied by [decl].
+
+   Return a universe context containing the local universes of [ctx]
+   and their constraints. The universes corresponding to
+   [decl.univdecl_instance] come first in the order defined by that
+   list. *)
 val check_univ_decl : t -> universe_decl -> Univ.UContext.t
 
 (** {5 TODO: Document me} *)