[api] Remove yet another type alias.

10 files changed, 46 insertions, 46 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 652ed0f9f..7cc541258 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -152,9 +152,9 @@ exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> Constant.t puniverses -> constr constrained
 val constant_type : env -> Constant.t puniverses -> types constrained
 
-val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.constraints) option
+val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.Constraint.t) option
 val constant_value_and_type : env -> Constant.t puniverses -> 
-  constr option * types * Univ.constraints
+  constr option * types * Univ.Constraint.t
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
 val constant_context : env -> Constant.t -> Univ.AUContext.t
@@ -203,10 +203,10 @@ val lookup_modtype : ModPath.t -> env -> module_type_body
 (** Add universe constraints to the environment.
     @raises UniverseInconsistency
 *)
-val add_constraints : Univ.constraints -> env -> env
+val add_constraints : Univ.Constraint.t -> env -> env
 
 (** Check constraints are satifiable in the environment. *)
-val check_constraints : Univ.constraints -> env -> bool
+val check_constraints : Univ.Constraint.t -> env -> bool
 val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
 val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index a19f87b05..8aaeee831 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -37,7 +37,7 @@ val ind_subst : MutInd.t -> mutual_inductive_body -> Instance.t -> constr list
 val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t
 
 val instantiate_inductive_constraints :
-  mutual_inductive_body -> Instance.t -> constraints
+  mutual_inductive_body -> Instance.t -> Constraint.t
 
 val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
 val constrained_type_of_inductive_knowing_parameters :
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 41d6c05eb..b0f4a1e5f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -212,7 +212,7 @@ type 'a universe_state = 'a * 'a universe_compare
 
 type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
 
-type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints
+type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 
 let sort_cmp_universes env pb s0 s1 (u, check) =
   (check.compare env pb s0 s1 u, check)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 05a906e28..573e4c8bd 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -49,7 +49,7 @@ type 'a universe_state = 'a * 'a universe_compare
 
 type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
 
-type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints
+type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 
 val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t ->
   'a * 'a universe_compare -> 'a * 'a universe_compare
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 0bfe07486..a30bb37e6 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -139,7 +139,7 @@ val push_context :
   bool -> Univ.UContext.t -> safe_transformer0
 
 val add_constraints :
-  Univ.constraints -> safe_transformer0
+  Univ.Constraint.t -> safe_transformer0
 
 (* (\** Generator of universes *\) *)
 (* val next_universe : int safe_transformer *)
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index b24c20aa0..67df3759e 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -10,4 +10,4 @@ open Univ
 open Declarations
 open Environ
 
-val check_subtypes : env -> module_type_body -> module_type_body -> constraints
+val check_subtypes : env -> module_type_body -> module_type_body -> Constraint.t
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 3a1f2ae00..781c6bfbc 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -59,7 +59,7 @@ type ('constr, 'types) ptype_error =
   | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array
   | IllTypedRecBody of
       int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
-  | UnsatisfiedConstraints of Univ.constraints
+  | UnsatisfiedConstraints of Univ.Constraint.t
 
 type type_error = (constr, types) ptype_error
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index e4fa65686..72861f6e4 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -60,7 +60,7 @@ type ('constr, 'types) ptype_error =
   | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array
   | IllTypedRecBody of
       int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
-  | UnsatisfiedConstraints of Univ.constraints
+  | UnsatisfiedConstraints of Univ.Constraint.t
 
 type type_error = (constr, types) ptype_error
 
@@ -105,4 +105,4 @@ val error_ill_typed_rec_body  :
 
 val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
 
-val error_unsatisfied_constraints : env -> Univ.constraints -> 'a
+val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index b95388ed0..f71d83d85 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -35,10 +35,10 @@ val check_eq_instances : Instance.t check_function
   constraints are not satisfiable. *)
 
 val enforce_constraint : univ_constraint -> t -> t
-val merge_constraints : constraints -> t -> t
+val merge_constraints : Constraint.t -> t -> t
 
 val check_constraint  : t -> univ_constraint -> bool
-val check_constraints : constraints -> t -> bool
+val check_constraints : Constraint.t -> t -> bool
 
 (** Adds a universe to the graph, ensuring it is >= or > Set.
    @raises AlreadyDeclared if the level is already declared in the graph. *)
@@ -57,7 +57,7 @@ val empty_universes : t
 
 val sort_universes : t -> t
 
-val constraints_of_universes : t -> constraints
+val constraints_of_universes : t -> Constraint.t
 
 val check_subtype : AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
diff --git a/kernel/univ.mli b/kernel/univ.mli
index f74f29b2c..459394439 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -169,20 +169,20 @@ module Constraint : sig
 end
 
 type constraints = Constraint.t
+[@@ocaml.deprecated "Use Constraint.t"]
 
-val empty_constraint : constraints
-val union_constraint : constraints -> constraints -> constraints
-val eq_constraint : constraints -> constraints -> bool
+val empty_constraint : Constraint.t
+val union_constraint : Constraint.t -> Constraint.t -> Constraint.t
+val eq_constraint : Constraint.t -> Constraint.t -> bool
 
-(** A value with universe constraints. *)
-type 'a constrained = 'a * constraints
+(** A value with universe Constraint.t. *)
+type 'a constrained = 'a * Constraint.t
 
 (** Constrained *)
-val constraints_of : 'a constrained -> constraints
+val constraints_of : 'a constrained -> Constraint.t
 
-(** Enforcing constraints. *)
-
-type 'a constraint_function = 'a -> 'a -> constraints -> constraints
+(** Enforcing Constraint.t. *)
+type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t
 
 val enforce_eq : Universe.t constraint_function
 val enforce_leq : Universe.t constraint_function
@@ -199,7 +199,7 @@ val enforce_leq_level : Level.t constraint_function
   universes in the path are canonical. Note that each step does not
   necessarily correspond to an actual constraint, but reflect how the
   system stores the graph and may result from combination of several
-  constraints...
+  Constraint.t...
 *)
 type explanation = (constraint_type * Universe.t) list
 type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option
@@ -294,8 +294,8 @@ val in_punivs : 'a -> 'a puniverses
 
 val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
 
-(** A vector of universe levels with universe constraints,
-    representiong local universe variables and associated constraints *)
+(** A vector of universe levels with universe Constraint.t,
+    representiong local universe variables and associated Constraint.t *)
 
 module UContext :
 sig
@@ -307,9 +307,9 @@ sig
   val is_empty : t -> bool
 
   val instance : t -> Instance.t
-  val constraints : t -> constraints
+  val constraints : t -> Constraint.t
 
-  val dest : t -> Instance.t * constraints
+  val dest : t -> Instance.t * Constraint.t
 
   (** Keeps the order of the instances *)
   val union : t -> t -> t
@@ -328,7 +328,7 @@ sig
 
   val repr : t -> UContext.t
   (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of
-      the context and [cstr] the abstracted constraints. *)
+      the context and [cstr] the abstracted Constraint.t. *)
 
   val empty : t
   val is_empty : t -> bool
@@ -342,7 +342,7 @@ sig
   val union : t -> t -> t
 
   val instantiate : Instance.t -> t -> Constraint.t
-  (** Generate the set of instantiated constraints **)
+  (** Generate the set of instantiated Constraint.t **)
 
 end
 
@@ -350,14 +350,14 @@ type abstract_universe_context = AUContext.t
 [@@ocaml.deprecated "Use AUContext.t"]
 
 (** Universe info for inductive types: A context of universe levels
-    with universe constraints, representing local universe variables
-    and constraints, together with a context of universe levels with
-    universe constraints, representing conditions for subtyping used
+    with universe Constraint.t, representing local universe variables
+    and Constraint.t, together with a context of universe levels with
+    universe Constraint.t, representing conditions for subtyping used
     for inductive types.
 
     This data structure maintains the invariant that the context for
-    subtyping constraints is exactly twice as big as the context for
-    universe constraints. *)
+    subtyping Constraint.t is exactly twice as big as the context for
+    universe Constraint.t. *)
 module CumulativityInfo :
 sig
   type t
@@ -370,7 +370,7 @@ sig
   val univ_context : t -> UContext.t
   val subtyp_context : t -> UContext.t
 
-  (** This function takes a universe context representing constraints
+  (** This function takes a universe context representing Constraint.t
       of an inductive and a Instance.t of fresh universe names for the
       subtyping (with the same length as the context in the given
       universe context) and produces a UInfoInd.t that with the
@@ -417,7 +417,7 @@ sig
 
   val diff : t -> t -> t
   val add_universe : Level.t -> t -> t
-  val add_constraints : constraints -> t -> t
+  val add_constraints : Constraint.t -> t -> t
   val add_instance : Instance.t -> t -> t
 
   (** Arbitrary choice of linear order of the variables *)
@@ -425,14 +425,14 @@ sig
   val to_context : t -> UContext.t
   val of_context : UContext.t -> t
 
-  val constraints : t -> constraints
+  val constraints : t -> Constraint.t
   val levels : t -> LSet.t
 
   (** the number of universes in the context *)
   val size : t -> int
 end
 
-(** A set of universes with universe constraints.
+(** A set of universes with universe Constraint.t.
     We linearize the set to a list after typechecking.
     Beware, representation could change.
 *)
@@ -449,7 +449,7 @@ val is_empty_level_subst : universe_level_subst -> bool
 (** Substitution of universes. *)
 val subst_univs_level_level : universe_level_subst -> Level.t -> Level.t
 val subst_univs_level_universe : universe_level_subst -> Universe.t -> Universe.t
-val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
+val subst_univs_level_constraints : universe_level_subst -> Constraint.t -> Constraint.t
 val subst_univs_level_abstract_universe_context :
   universe_level_subst -> AUContext.t -> AUContext.t
 val subst_univs_level_instance : universe_level_subst -> Instance.t -> Instance.t
@@ -461,7 +461,7 @@ val is_empty_subst : universe_subst -> bool
 val make_subst : universe_subst -> universe_subst_fn
 
 val subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t
-val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
+val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
 
 (** Substitution of instances *)
 val subst_instance_instance : Instance.t -> Instance.t -> Instance.t
@@ -479,7 +479,7 @@ val make_abstract_instance : AUContext.t -> Instance.t
 (** {6 Pretty-printing of universes. } *)
 
 val pr_constraint_type : constraint_type -> Pp.t
-val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t
+val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t
 val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t
 val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t
 val pr_abstract_universe_context : (Level.t -> Pp.t) -> AUContext.t -> Pp.t
@@ -494,7 +494,7 @@ val pr_universe_subst : universe_subst -> Pp.t
 (** {6 Hash-consing } *)
 
 val hcons_univ : Universe.t -> Universe.t
-val hcons_constraints : constraints -> constraints
+val hcons_constraints : Constraint.t -> Constraint.t
 val hcons_universe_set : LSet.t -> LSet.t
 val hcons_universe_context : UContext.t -> UContext.t
 val hcons_abstract_universe_context : AUContext.t -> AUContext.t
@@ -515,6 +515,6 @@ val eq_levels : Level.t -> Level.t -> bool
 val equal_universes : Universe.t -> Universe.t -> bool
 [@@ocaml.deprecated "Use Universe.equal"]
 
-(** Universes of constraints *)
-val universes_of_constraints : constraints -> LSet.t
+(** Universes of Constraint.t *)
+val universes_of_constraints : Constraint.t -> LSet.t
 [@@ocaml.deprecated "Use Constraint.universes_of"]