[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.

9 files changed, 5 insertions, 106 deletions

diff --git a/kernel/constr.mli b/kernel/constr.mli
index 2efdae007c..3c9cc96a0d 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -13,20 +13,12 @@
 
 open Names
 
-(** {6 Value under universe substitution } *)
-type 'a puniverses = 'a Univ.puniverses
-[@@ocaml.deprecated "use Univ.puniverses"]
-
 (** {6 Simply type aliases } *)
 type pconstant = Constant.t Univ.puniverses
 type pinductive = inductive Univ.puniverses
 type pconstructor = constructor Univ.puniverses
 
 (** {6 Existential variables } *)
-type existential_key = Evar.t
-[@@ocaml.deprecated "use Evar.t"]
-
-(** {6 Existential variables } *)
 type metavariable = int
 
 (** {6 Case annotation } *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 1343b9029b..55ff7ff162 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -320,8 +320,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
 open Retroknowledge
 (** functions manipulating the retroknowledge 
     @author spiwack *)
-val retroknowledge : (retroknowledge->'a) -> env -> 'a
-[@@ocaml.deprecated "Use the record projection."]
 
 val registered : env -> field -> bool
 
diff --git a/kernel/names.ml b/kernel/names.ml
index 1e28ec51fb..7cd749de1d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -739,15 +739,12 @@ let eq_table_key f ik1 ik2 =
   | RelKey k1, RelKey k2 -> Int.equal k1 k2
   | _ -> false
 
-let eq_con_chk = Constant.UserOrd.equal
 let eq_mind_chk = MutInd.UserOrd.equal
 let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2
 
-
 (*******************************************************************)
 (** Compatibility layers *)
 
-type mod_bound_id = MBId.t
 let eq_constant_key = Constant.UserOrd.equal
 
 (** Compatibility layer for [ModPath] *)
@@ -923,8 +920,6 @@ struct
 
 end
 
-type projection = Projection.t
-
 module GlobRefInternal = struct
 
   type t =
@@ -1015,10 +1010,6 @@ module GlobRef = struct
 
 end
 
-type global_reference = GlobRef.t
-[@@ocaml.deprecated "Alias for [GlobRef.t]"]
-
-
 type evaluable_global_reference =
   | EvalVarRef of Id.t
   | EvalConstRef of Constant.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 2145a51c4e..37930c12e2 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -527,15 +527,8 @@ val eq_constant_key : Constant.t -> Constant.t -> bool
 
 (** equalities on constant and inductive names (for the checker) *)
 
-val eq_con_chk : Constant.t -> Constant.t -> bool
-[@@ocaml.deprecated "Same as [Constant.UserOrd.equal]."]
-
 val eq_ind_chk : inductive -> inductive -> bool
 
-(** {6 Deprecated functions. For backward compatibility.} *)
-
-type mod_bound_id = MBId.t
-[@@ocaml.deprecated "Same as [MBId.t]."]
 (** {5 Module paths} *)
 
 type module_path = ModPath.t =
@@ -625,9 +618,6 @@ module Projection : sig
 
 end
 
-type projection = Projection.t
-[@@ocaml.deprecated "Alias for [Projection.t]"]
-
 (** {6 Global reference is a kernel side type for all references together } *)
 
 (* XXX: Should we define GlobRefCan GlobRefUser? *)
@@ -665,9 +655,6 @@ module GlobRef : sig
 
 end
 
-type global_reference = GlobRef.t
-[@@ocaml.deprecated "Alias for [GlobRef.t]"]
-
 (** Better to have it here that in Closure, since required in grammar.cma *)
 (* XXX: Move to a module *)
 type evaluable_global_reference =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b03342da39..820c5b3a2b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -883,12 +883,6 @@ let typing senv = Typeops.infer (env_of_senv senv)
 
 (** {6 Retroknowledge / native compiler } *)
 
-[@@@ocaml.warning "-3"]
-(** universal lifting, used for the "get" operations mostly *)
-let retroknowledge f senv =
-  Environ.retroknowledge f (env_of_senv senv)
-[@@@ocaml.warning "+3"]
-
 let register field value senv =
   (* todo : value closed *)
   (* spiwack : updates the safe_env with the information that the register
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index efb4957006..0f150ea971 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -208,9 +208,6 @@ val delta_of_senv :
 
 open Retroknowledge
 
-val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
-[@@ocaml.deprecated "Use the projection of Environ.env"]
-
 val register :
   field -> GlobRef.t -> safe_transformer0
 
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 752bf76270..4336a22b8c 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -12,8 +12,6 @@ open Univ
 
 (** {6 Graphs of universes. } *)
 type t
-type universes = t
-[@@ocaml.deprecated "Use UGraph.t"]
 
 type 'a check_function = t -> 'a -> 'a -> bool
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 61ad1d0a82..fa37834a23 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -574,11 +574,8 @@ struct
       pp_std ++ prl u1 ++ pr_constraint_type op ++
 	prl u2 ++ fnl () )  c (str "")
 
-  let universes_of c =
-    fold (fun (u1, _op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty
 end
 
-let universes_of_constraints = Constraint.universes_of
 let empty_constraint = Constraint.empty
 let union_constraint = Constraint.union
 let eq_constraint = Constraint.equal
@@ -897,8 +894,6 @@ let subst_instance_constraints s csts =
     (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
     csts Constraint.empty 
 
-type universe_instance = Instance.t
-
 type 'a puniverses = 'a * Instance.t
 let out_punivs (x, _y) = x
 let in_punivs x = (x, Instance.empty)
@@ -955,7 +950,6 @@ struct
 
 end
 
-type abstract_universe_context = AUContext.t
 let hcons_abstract_universe_context = AUContext.hcons
 
 (** Universe info for cumulative inductive types: A context of
@@ -997,12 +991,10 @@ struct
 
 end
 
-type cumulativity_info = CumulativityInfo.t
 let hcons_cumulativity_info = CumulativityInfo.hcons
 
 module ACumulativityInfo = CumulativityInfo
 
-type abstract_cumulativity_info = ACumulativityInfo.t
 let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
 
 (** A set of universes with universe constraints.
@@ -1238,7 +1230,3 @@ let explain_universe_inconsistency prl (o,u,v,p) =
   in
     str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
       pr_rel o ++ spc() ++ pr_uni v ++ reason
-
-let compare_levels = Level.compare
-let eq_levels = Level.equal
-let equal_universes = Universe.equal
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"]