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

4 files changed, 0 insertions, 164 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index aa9bd20bf3..4f0bf1b5d2 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -533,7 +533,3 @@ let save_proof ?proof = function
       (* if the proof is given explicitly, nothing has to be deleted *)
       if Option.is_empty proof then Proof_global.discard_current ();
       Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
-
-(* Miscellaneous *)
-let get_current_context () = Pfedit.get_current_context ()
-
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 38683ed6b2..62b25946d9 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -67,10 +67,3 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 val set_save_hook : (Proof.t -> unit) -> unit
 
 val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
-
-(** [get_current_context ()] returns the evar context and env of the
-   current open proof if any, otherwise returns the empty evar context
-   and the current global env *)
-
-val get_current_context : unit -> Evd.evar_map * Environ.env
-[@@ocaml.deprecated "please use [Pfedit.get_current_context]"]
diff --git a/vernac/misctypes.ml b/vernac/misctypes.ml
deleted file mode 100644
index ef9cd3c351..0000000000
--- a/vernac/misctypes.ml
+++ /dev/null
@@ -1,75 +0,0 @@
-(* Compat module, to be removed in 8.10 *)
-open Names
-
-type lident = Names.lident
-[@@ocaml.deprecated "use [Names.lident"]
-type lname = Names.lname
-[@@ocaml.deprecated "use [Names.lname]"]
-type lstring = Names.lstring
-[@@ocaml.deprecated "use [Names.lstring]"]
-
-type 'a or_by_notation_r = 'a Constrexpr.or_by_notation_r =
-  | AN of 'a [@ocaml.deprecated "use version in [Constrexpr]"]
-  | ByNotation of (string * string option) [@ocaml.deprecated "use version in [Constrexpr]"]
-[@@ocaml.deprecated "use [Constrexpr.or_by_notation_r]"]
-
-type 'a or_by_notation = 'a Constrexpr.or_by_notation
-[@@ocaml.deprecated "use [Constrexpr.or_by_notation]"]
-
-type intro_pattern_naming_expr = Namegen.intro_pattern_naming_expr =
-  | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Namegen]"]
-  | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Namegen]"]
-  | IntroAnonymous [@ocaml.deprecated "Use version in [Namegen]"]
-[@@ocaml.deprecated "use [Namegen.intro_pattern_naming_expr]"]
-
-type 'a or_var = 'a Locus.or_var =
-  | ArgArg of 'a [@ocaml.deprecated "Use version in [Locus]"]
-  | ArgVar of Names.lident [@ocaml.deprecated "Use version in [Locus]"]
-[@@ocaml.deprecated "use [Locus.or_var]"]
-
-type quantified_hypothesis = Tactypes.quantified_hypothesis =
-    AnonHyp of int [@ocaml.deprecated "Use version in [Tactypes]"]
-  | NamedHyp of Id.t [@ocaml.deprecated "Use version in [Tactypes]"]
-[@@ocaml.deprecated "use [Tactypes.quantified_hypothesis]"]
-
-type multi = Equality.multi =
-  | Precisely of int [@ocaml.deprecated "use version in [Equality]"]
-  | UpTo of int [@ocaml.deprecated "use version in [Equality]"]
-  | RepeatStar [@ocaml.deprecated "use version in [Equality]"]
-  | RepeatPlus [@ocaml.deprecated "use version in [Equality]"]
-[@@ocaml.deprecated "use [Equality.multi]"]
-
-type 'a bindings = 'a Tactypes.bindings =
-  | ImplicitBindings of 'a list [@ocaml.deprecated "use version in [Tactypes]"]
-  | ExplicitBindings of 'a Tactypes.explicit_bindings [@ocaml.deprecated "use version in [Tactypes]"]
-  | NoBindings [@ocaml.deprecated "use version in [Tactypes]"]
-[@@ocaml.deprecated "use [Tactypes.bindings]"]
-
-type 'constr intro_pattern_expr = 'constr Tactypes.intro_pattern_expr =
-  | IntroForthcoming of bool [@ocaml.deprecated "use version in [Tactypes]"]
-  | IntroNaming of Namegen.intro_pattern_naming_expr [@ocaml.deprecated "use version in [Tactypes]"]
-  | IntroAction of 'constr Tactypes.intro_pattern_action_expr [@ocaml.deprecated "use version in [Tactypes]"]
-and 'constr intro_pattern_action_expr = 'constr Tactypes.intro_pattern_action_expr =
-  | IntroWildcard [@ocaml.deprecated "use [Tactypes]"]
-  | IntroOrAndPattern of 'constr Tactypes.or_and_intro_pattern_expr [@ocaml.deprecated "use [Tactypes]"]
-  | IntroInjection of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"]
-  | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t [@ocaml.deprecated "use [Tactypes]"]
-  | IntroRewrite of bool [@ocaml.deprecated "use [Tactypes]"]
-and 'constr or_and_intro_pattern_expr = 'constr Tactypes.or_and_intro_pattern_expr =
-  | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list [@ocaml.deprecated "use [Tactypes]"]
-  | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"]
-[@@ocaml.deprecated "use version in [Tactypes]"]
-
-type 'id move_location = 'id Logic.move_location =
-  | MoveAfter of 'id [@ocaml.deprecated "use version in [Logic]"]
-  | MoveBefore of 'id [@ocaml.deprecated "use version in [Logic]"]
-  | MoveFirst [@ocaml.deprecated "use version in [Logic]"]
-  | MoveLast [@ocaml.deprecated "use version in [Logic]"]
-[@@ocaml.deprecated "use version in [Logic]"]
-
-type 'a cast_type = 'a Glob_term.cast_type =
-  | CastConv of 'a [@ocaml.deprecated "use version in [Glob_term]"]
-  | CastVM of 'a [@ocaml.deprecated "use version in [Glob_term]"]
-  | CastCoerce [@ocaml.deprecated "use version in [Glob_term]"]
-  | CastNative of 'a [@ocaml.deprecated "use version in [Glob_term]"]
-[@@ocaml.deprecated "use version in [Glob_term]"]
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index a5601d8c85..a2ea706b75 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -15,14 +15,6 @@ open Libnames
 (** Vernac expressions, produced by the parser *)
 type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation
 
-type goal_selector = Goal_select.t =
-  | SelectAlreadyFocused [@ocaml.deprecated "Use Goal_select.SelectAlreadyFocused"]
-  | SelectNth of int [@ocaml.deprecated "Use Goal_select.SelectNth"]
-  | SelectList of (int * int) list [@ocaml.deprecated "Use Goal_select.SelectList"]
-  | SelectId of Id.t [@ocaml.deprecated "Use Goal_select.SelectId"]
-  | SelectAll [@ocaml.deprecated "Use Goal_select.SelectAll"]
-[@@ocaml.deprecated "Use Goal_select.t"]
-
 type goal_identifier = string
 type scope_name = string
 
@@ -31,9 +23,6 @@ type goal_reference =
   | NthGoal of int
   | GoalId of Id.t
 
-type univ_name_list = UnivNames.univ_name_list
-[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
-
 type printable =
   | PrintTables
   | PrintFullContext
@@ -102,54 +91,12 @@ type comment =
   | CommentString of string
   | CommentInt of int
 
-type reference_or_constr = Hints.reference_or_constr =
-  | HintsReference of qualid [@ocaml.deprecated "Use Hints.HintsReference"]
-  | HintsConstr of constr_expr [@ocaml.deprecated "Use Hints.HintsConstr"]
-[@@ocaml.deprecated "Please use [Hints.reference_or_constr]"]
-
-type hint_mode = Hints.hint_mode =
-  | ModeInput [@ocaml.deprecated "Use Hints.ModeInput"]
-  | ModeNoHeadEvar [@ocaml.deprecated "Use Hints.ModeNoHeadEvar"]
-  | ModeOutput [@ocaml.deprecated "Use Hints.ModeOutput"]
-[@@ocaml.deprecated "Please use [Hints.hint_mode]"]
-
-type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
-    { hint_priority : int option; [@ocaml.deprecated "Use Typeclasses.hint_priority"]
-      hint_pattern : 'a option [@ocaml.deprecated "Use Typeclasses.hint_pattern"] }
-[@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"]
-
-type hint_info_expr = Hints.hint_info_expr
-[@@ocaml.deprecated "Please use [Hints.hint_info_expr]"]
-
-type hints_expr = Hints.hints_expr =
-  | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
-        [@ocaml.deprecated "Use the constructor in module [Hints]"]
-  | HintsResolveIFF of bool * qualid list * int option
-        [@ocaml.deprecated "Use the constructor in module [Hints]"]
-  | HintsImmediate of Hints.reference_or_constr list
-        [@ocaml.deprecated "Use the constructor in module [Hints]"]
-  | HintsUnfold of qualid list
-        [@ocaml.deprecated "Use the constructor in module [Hints]"]
-  | HintsTransparency of qualid Hints.hints_transparency_target * bool
-        [@ocaml.deprecated "Use the constructor in module [Hints]"]
-  | HintsMode of qualid * Hints.hint_mode list
-                   [@ocaml.deprecated "Use the constructor in module [Hints]"]
-  | HintsConstructors of qualid list
-        [@ocaml.deprecated "Use the constructor in module [Hints]"]
-  | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
-        [@ocaml.deprecated "Use the constructor in module [Hints]"]
-[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
-
 type search_restriction =
   | SearchInside of qualid list
   | SearchOutside of qualid list
 
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
-type opacity_flag   = Proof_global.opacity_flag =
-    Opaque [@ocaml.deprecated "Use Proof_global.Opaque"]
-  | Transparent [@ocaml.deprecated "Use Proof_global.Transparent"]
- [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"]
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
@@ -285,33 +232,8 @@ type register_kind =
   | RegisterInline
   | RegisterRetroknowledge of qualid
 
-type bullet = Proof_bullet.t
-[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"]
-
 (** {6 Types concerning the module layer} *)
 
-(** Rigid / flexible module signature *)
-
-type 'a module_signature = 'a Declaremods.module_signature =
-  | Enforce of 'a (** ... : T *)
-        [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
-  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
-        [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
-[@@ocaml.deprecated "please use [Declaremods.module_signature]."]
-
-(** Which module inline annotations should we honor,
-    either None or the ones whose level is less or equal
-    to the given integer *)
-
-type inline = Declaremods.inline =
-  | NoInline
-      [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
-  | DefaultInline
-      [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
-  | InlineAt of int
-      [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
-[@@ocaml.deprecated "please use [Declaremods.inline]."]
-
 type module_ast_inl = module_ast * Declaremods.inline
 type module_binder = bool option * lident list * module_ast_inl