[api] Remove (most) 8.9 deprecated objects.

A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.

1 files changed, 5 insertions, 51 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
index b68bbdf359..1aa53b8aa8 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -51,9 +51,6 @@ sig
   val name : t -> (Names.DirPath.t * int) option
 end
 
-type universe_level = Level.t
-[@@ocaml.deprecated "Use Level.t"]
-
 (** Sets of universe levels *)
 module LSet :
 sig
@@ -63,9 +60,6 @@ sig
   (** Pretty-printing *)
 end
 
-type universe_set = LSet.t
-[@@ocaml.deprecated "Use LSet.t"]
-
 module Universe :
 sig
   type t
@@ -130,9 +124,6 @@ sig
 
 end
 
-type universe = Universe.t
-[@@ocaml.deprecated "Use Universe.t"]
-
 (** Alias name. *)
 
 val pr_uni : Universe.t -> Pp.t
@@ -171,9 +162,6 @@ module Constraint : sig
  include Set.S with type elt = univ_constraint
 end
 
-type constraints = Constraint.t
-[@@ocaml.deprecated "Use Constraint.t"]
-
 val empty_constraint : Constraint.t
 val union_constraint : Constraint.t -> Constraint.t -> Constraint.t
 val eq_constraint : Constraint.t -> Constraint.t -> bool
@@ -301,9 +289,6 @@ sig
 
 end
 
-type universe_instance = Instance.t
-[@@ocaml.deprecated "Use Instance.t"]
-
 val enforce_eq_instances : Instance.t constraint_function
 
 val enforce_eq_variance_instances : Variance.t array -> Instance.t constraint_function
@@ -340,9 +325,6 @@ sig
 
 end
 
-type universe_context = UContext.t
-[@@ocaml.deprecated "Use UContext.t"]
-
 module AUContext :
 sig
   type t
@@ -367,9 +349,6 @@ sig
 
 end
 
-type abstract_universe_context = AUContext.t
-[@@ocaml.deprecated "Use AUContext.t"]
-
 (** Universe info for cumulative inductive types: A context of
    universe levels with universe constraints, representing local
    universe variables and constraints, together with an array of
@@ -398,9 +377,6 @@ sig
   val eq_constraints : t -> Instance.t constraint_function
 end
 
-type cumulativity_info = CumulativityInfo.t
-[@@ocaml.deprecated "Use CumulativityInfo.t"]
-
 module ACumulativityInfo :
 sig
   type t
@@ -411,11 +387,13 @@ sig
   val eq_constraints : t -> Instance.t constraint_function
 end
 
-type abstract_cumulativity_info = ACumulativityInfo.t
-[@@ocaml.deprecated "Use ACumulativityInfo.t"]
-
 (** Universe contexts (as sets) *)
 
+(** A set of universes with universe Constraint.t.
+    We linearize the set to a list after typechecking.
+    Beware, representation could change.
+*)
+
 module ContextSet :
 sig
   type t = LSet.t constrained
@@ -451,13 +429,6 @@ sig
   val size : t -> int
 end
 
-(** A set of universes with universe Constraint.t.
-    We linearize the set to a list after typechecking.
-    Beware, representation could change.
-*)
-type universe_context_set = ContextSet.t
-[@@ocaml.deprecated "Use ContextSet.t"]
-
 (** A value in a universe context (resp. context set). *)
 type 'a in_universe_context = 'a * UContext.t
 type 'a in_universe_context_set = 'a * ContextSet.t
@@ -532,20 +503,3 @@ val hcons_abstract_universe_context : AUContext.t -> AUContext.t
 val hcons_universe_context_set : ContextSet.t -> ContextSet.t
 val hcons_cumulativity_info : CumulativityInfo.t -> CumulativityInfo.t
 val hcons_abstract_cumulativity_info : ACumulativityInfo.t -> ACumulativityInfo.t
-
-(******)
-
-(* deprecated: use qualified names instead *)
-val compare_levels : Level.t -> Level.t -> int
-[@@ocaml.deprecated "Use Level.compare"]
-
-val eq_levels : Level.t -> Level.t -> bool
-[@@ocaml.deprecated "Use Level.equal"]
-
-(** deprecated: Equality of formal universe expressions. *)
-val equal_universes : Universe.t -> Universe.t -> bool
-[@@ocaml.deprecated "Use Universe.equal"]
-
-(** Universes of Constraint.t *)
-val universes_of_constraints : Constraint.t -> LSet.t
-[@@ocaml.deprecated "Use Constraint.universes_of"]