Merge PR #6368: [api] Remove yet another type alias.

4 files changed, 18 insertions, 16 deletions

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 651ccbb10..f54c422ad 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -187,9 +187,9 @@ val whd_evar : Evd.evar_map -> constr -> constr
 
 val eq_constr : Evd.evar_map -> t -> t -> bool
 val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
-val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
-val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
-val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option
+val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
 val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 
 (** {6 Iterators} *)
diff --git a/engine/evd.mli b/engine/evd.mli
index fb5a6cd16..636bd1be1 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -208,7 +208,7 @@ val is_defined : evar_map -> Evar.t-> bool
 val is_undefined : evar_map -> Evar.t-> bool
 (** Whether an evar is not defined in an evarmap. *)
 
-val add_constraints : evar_map -> Univ.constraints -> evar_map
+val add_constraints : evar_map -> Univ.Constraint.t -> evar_map
 (** Add universe constraints in an evar map. *)
 
 val undefined_map : evar_map -> evar_info Evar.Map.t
@@ -316,7 +316,7 @@ val whd_sort_variable : evar_map -> constr -> constr
 
 exception UniversesDiffer
 
-val add_universe_constraints : evar_map -> Universes.universe_constraints -> evar_map
+val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map
 (** Add the given universe unification constraints to the evar map.
     @raises UniversesDiffer in case a first-order unification fails.
     @raises UniverseInconsistency
@@ -491,7 +491,7 @@ val univ_flexible_alg : rigid
 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_universe_context_constraints : UState.t -> Univ.Constraint.t
 val evar_context_universe_context : UState.t -> Univ.UContext.t
 [@@ocaml.deprecated "alias of UState.context"]
 
@@ -513,7 +513,7 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 
 val universe_binders : evar_map -> Universes.universe_binders
 val add_constraints_context : UState.t ->
-  Univ.constraints -> UState.t
+  Univ.Constraint.t -> UState.t
 
 
 val normalize_evar_universe_context_variables : UState.t -> 
diff --git a/engine/uState.mli b/engine/uState.mli
index 5dfe9a22d..6657d6047 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -53,7 +53,7 @@ val algebraics : t -> Univ.LSet.t
 (** The subset of unification variables that can be instantiated with algebraic
     universes as they appear in inferred types only. *)
 
-val constraints : t -> Univ.constraints
+val constraints : t -> Univ.Constraint.t
 (** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *)
 
 val context : t -> Univ.UContext.t
@@ -68,12 +68,12 @@ val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
 
 (** {5 Constraints handling} *)
 
-val add_constraints : t -> Univ.constraints -> t
+val add_constraints : t -> Univ.Constraint.t -> t
 (**
   @raise UniversesDiffer when universes differ
 *)
 
-val add_universe_constraints : t -> Universes.universe_constraints -> t
+val add_universe_constraints : t -> Universes.Constraints.t -> t
 (**
   @raise UniversesDiffer when universes differ
 *)
diff --git a/engine/universes.mli b/engine/universes.mli
index fc9278eb5..1a98d969b 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -74,21 +74,23 @@ type universe_constraint_type = ULe | UEq | ULub
 type universe_constraint = Universe.t * universe_constraint_type * Universe.t
 module Constraints : sig
   include Set.S with type elt = universe_constraint
-		       
+
   val pr : t -> Pp.t
 end
 
 type universe_constraints = Constraints.t
-type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option
-type 'a universe_constrained = 'a * universe_constraints
-type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
+[@@ocaml.deprecated "Use Constraints.t"]
+
+type 'a constraint_accumulator = Constraints.t -> 'a -> 'a option
+type 'a universe_constrained = 'a * Constraints.t
+type 'a universe_constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t
 
 val subst_univs_universe_constraints : universe_subst_fn -> 
-  universe_constraints -> universe_constraints
+  Constraints.t -> Constraints.t
 
 val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function
 
-val to_constraints : UGraph.t -> universe_constraints -> constraints
+val to_constraints : UGraph.t -> Constraints.t -> Constraint.t
 
 (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
     {!eq_constr_univs_infer} taking kind-of-term functions, to expose