Merge PR #9887: [api] Remove 8.10 deprecations.

Reviewed-by: SkySkimmer

48 files changed, 47 insertions, 536 deletions

diff --git a/clib/cString.ml b/clib/cString.ml
index 111be3da82..423c08da13 100644
--- a/clib/cString.ml
+++ b/clib/cString.ml
@@ -17,16 +17,12 @@ sig
   val is_empty : string -> bool
   val explode : string -> string list
   val implode : string list -> string
-  val strip : string -> string
-  [@@ocaml.deprecated "Use [trim]"]
   val drop_simple_quotes : string -> string
   val string_index_from : string -> int -> string -> int
   val string_contains : where:string -> what:string -> bool
   val plural : int -> string -> string
   val conjugate_verb_to_be : int -> string
   val ordinal : int -> string
-  val split : char -> string -> string list
-  [@@ocaml.deprecated "Use [split_on_char]"]
   val is_sub : string -> string -> int -> bool
   module Set : Set.S with type elt = t
   module Map : CMap.ExtS with type key = t and module Set := Set
@@ -59,8 +55,6 @@ let implode sl = String.concat "" sl
 
 let is_empty s = String.length s = 0
 
-let strip = String.trim
-
 let drop_simple_quotes s =
   let n = String.length s in
   if n > 2 && s.[0] = '\'' && s.[n-1] = '\'' then String.sub s 1 (n-2) else s
@@ -124,8 +118,6 @@ let ordinal n =
 
 (* string parsing *)
 
-let split = String.split_on_char
-
 module Self =
 struct
   type t = string
diff --git a/clib/cString.mli b/clib/cString.mli
index 364b6a34b1..f68bd3bb65 100644
--- a/clib/cString.mli
+++ b/clib/cString.mli
@@ -30,10 +30,6 @@ sig
   val implode : string list -> string
   (** [implode [s1; ...; sn]] returns [s1 ^ ... ^ sn] *)
 
-  val strip : string -> string
-  [@@ocaml.deprecated "Use [trim]"]
-  (** Alias for [String.trim] *)
-
   val drop_simple_quotes : string -> string
   (** Remove the eventual first surrounding simple quotes of a string. *)
 
@@ -52,10 +48,6 @@ sig
   val ordinal : int -> string
   (** Generate the ordinal number in English. *)
 
-  val split : char -> string -> string list
-  [@@ocaml.deprecated "Use [split_on_char]"]
-  (** [split c s] alias of [String.split_on_char] *)
-
   val is_sub : string -> string -> int -> bool
   (** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *)
 
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9e0d47651e..7221c3de56 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,10 @@
+## Changes between Coq 8.10 and Coq 8.11
+
+### ML API
+
+- Functions and types deprecated in 8.10 have been removed in Coq
+  8.11.
+
 ## Changes between Coq 8.9 and Coq 8.10
 
 ### ML4 Pre Processing
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 96beb72a56..be0318fbde 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -26,24 +26,7 @@ let safe_evar_value sigma ev =
   try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev)
   with NotInstantiatedEvar | Not_found -> None
 
-(** Combinators *)
-
-let evd_comb0 f evdref =
-  let (evd',x) = f !evdref in
-    evdref := evd';
-    x
-
-let evd_comb1 f evdref x =
-  let (evd',y) = f !evdref x in
-    evdref := evd';
-    y
-
-let evd_comb2 f evdref x y =
-  let (evd',z) = f !evdref x y in
-    evdref := evd';
-    z
-
-let new_global evd x = 
+let new_global evd x =
   let (evd, c) = Evd.fresh_global (Global.env()) evd x in
   (evd, c)
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index bb0da44103..8eaff8bd13 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -274,15 +274,6 @@ val push_rel_context_to_named_context : ?hypnaming:naming_mode ->
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 
-(** Evar combinators *)
-
-val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-
 val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
 
diff --git a/engine/evd.ml b/engine/evd.ml
index b89222cf8e..d37b49e2dc 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -869,8 +869,6 @@ let to_universe_context evd = UState.context evd.universes
 
 let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
 
-let const_univ_entry = univ_entry
-
 let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
 
 let restrict_universe_context evd vars =
diff --git a/engine/evd.mli b/engine/evd.mli
index b0fcddb068..29235050b0 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -615,9 +615,6 @@ val to_universe_context : evar_map -> Univ.UContext.t
 
 val univ_entry : poly:bool -> evar_map -> Entries.universes_entry
 
-val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry
-[@@ocaml.deprecated "Use [univ_entry]."]
-
 val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry
 
 val merge_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index ac0344148a..dab2e7d5ef 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -56,13 +56,6 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
 
 let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
 
-let nf_enter f =
-  bind goals
-    (fun gl ->
-      gl >>= fun gl ->
-      Proofview.Goal.normalize gl >>= fun nfgl ->
-      Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"]
-
 let enter f =
   bind goals
     (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 3c4fa6f4e8..ed95d62bc6 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -41,9 +41,6 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
 
 (** {5 Focussing} *)
 
-val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t
-[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
-
 (** Enter a goal. The resulting tactic is focussed. *)
 
 val enter : (Proofview.Goal.t -> 'a t) -> 'a t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index f278c83912..ecea637947 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1104,13 +1104,6 @@ module Goal = struct
         tclZERO ~info e
     end
     end
-
-  let normalize { self; state } =
-    Env.get >>= fun env ->
-    tclEVARMAP >>= fun sigma ->
-    let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in
-    tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
-
   let gmake env sigma goal =
     let state = get_state goal in
     let goal = drop_state goal in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 9455dae643..92f8b86df5 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -505,10 +505,6 @@ module Goal : sig
   (** Type of goals. *)
   type t
 
-  (** Normalises the argument goal. *)
-  val normalize : t -> t tactic
-  [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"]
-
   (** [concl], [hyps], [env] and [sigma] given a goal [gl] return
       respectively the conclusion of [gl], the hypotheses of [gl], the
       environment of [gl] (i.e. the global environment and the
diff --git a/engine/termops.ml b/engine/termops.ml
index 8e12c9be88..8a6bd17948 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -25,11 +25,6 @@ module CompactedDecl = Context.Compacted.Declaration
 
 module Internal = struct
 
-let pr_sort_family = Sorts.pr_sort_family
-[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
-let pr_fix = Constr.debug_print_fix
-[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-
 let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c)
 let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c)
 let term_printer = ref debug_print_constr_env
@@ -761,13 +756,6 @@ let fold_constr_with_binders sigma g f n acc c =
   let c = Unsafe.to_constr (whd_evar sigma c) in
   Constr.fold_constr_with_binders g f n acc c
 
-(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
-   subterms of [c]; it carries an extra data [acc] which is processed by [g] at
-   each binder traversal; it is not recursive and the order with which
-   subterms are processed is not specified *)
-
-let iter_constr_with_full_binders = EConstr.iter_with_full_binders
-
 (***************************)
 (* occurs check functions  *)
 (***************************)
@@ -862,8 +850,6 @@ let collect_vars sigma c =
   | _ -> EConstr.fold sigma aux vars c in
   aux Id.Set.empty c
 
-let vars_of_global_reference = vars_of_global
-
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
@@ -1417,10 +1403,6 @@ let prod_applist_assum sigma n c l =
     | _ -> anomaly (Pp.str "Not enough prod/let's.") in
   app n [] c l
 
-let on_judgment = Environ.on_judgment
-let on_judgment_value = Environ.on_judgment_value
-let on_judgment_type = Environ.on_judgment_type
-
 (* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
      variables skips let-in's; let-in's in the middle are put in ctx2 *)
 let context_chop k ctx =
diff --git a/engine/termops.mli b/engine/termops.mli
index 1dd9941c5e..a9217b3586 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -16,12 +16,6 @@ open Constr
 open Environ
 open EConstr
 
-(** printers *)
-val pr_sort_family : Sorts.family -> Pp.t
-[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
-val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
-[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-
 (** about contexts *)
 val push_rel_assum : Name.t Context.binder_annot * types -> env -> env
 val push_rels_assum : (Name.t Context.binder_annot * Constr.types) list -> env -> env
@@ -84,12 +78,6 @@ val fold_constr_with_full_binders : Evd.evar_map ->
   ('a -> 'b -> constr -> 'b) ->
   'a -> 'b -> constr -> 'b
 
-val iter_constr_with_full_binders : Evd.evar_map ->
-  (rel_declaration -> 'a -> 'a) ->
-  ('a -> constr -> unit) -> 'a ->
-  constr -> unit
-[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."]
-
 (**********************************************************************)
 
 val strip_head_cast : Evd.evar_map -> constr -> constr
@@ -121,9 +109,6 @@ val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
 val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
 
-val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
-[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
-
 (* Substitution of metavariables *)
 type meta_value_map = (metavariable * Constr.constr) list
 val subst_meta : meta_value_map -> Constr.constr -> Constr.constr
@@ -292,15 +277,6 @@ val is_Type : Evd.evar_map -> constr -> bool
 
 val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
 
-(** Combinators on judgments *)
-
-val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment]."]
-val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment_value]."]
-val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment_type]."]
-
 (** {5 Debug pretty-printers} *)
 
 open Evd
diff --git a/engine/uState.ml b/engine/uState.ml
index aa14f66df6..adea78d4c9 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -116,8 +116,6 @@ let univ_entry ~poly uctx =
     Polymorphic_entry (nas, uctx)
   else Monomorphic_entry (context_set uctx)
 
-let const_univ_entry = univ_entry
-
 let of_context_set ctx = { empty with uctx_local = ctx }
 
 let subst ctx = ctx.uctx_univ_variables
diff --git a/engine/uState.mli b/engine/uState.mli
index a358813825..3df7f9e8e9 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -67,9 +67,6 @@ val context : t -> Univ.UContext.t
 val univ_entry : poly:bool -> t -> Entries.universes_entry
 (** Pick from {!context} or {!context_set} based on [poly]. *)
 
-val const_univ_entry : poly:bool -> t -> Entries.universes_entry
-[@@ocaml.deprecated "Use [univ_entry]."]
-
 (** {5 Constraints handling} *)
 
 val drop_weak_constraints : bool ref
diff --git a/engine/univGen.ml b/engine/univGen.ml
index c310331b15..f1deb1bfaf 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -25,11 +25,6 @@ let new_univ_global () =
 let fresh_level () =
   Univ.Level.make (new_univ_global ())
 
-(* TODO: remove *)
-let new_univ () = Univ.Universe.make (fresh_level ())
-let new_Type () = mkType (new_univ ())
-let new_Type_sort () = sort_of_univ (new_univ ())
-
 let fresh_instance auctx =
   let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
   let ctx = Array.fold_right LSet.add inst LSet.empty in
@@ -83,10 +78,6 @@ let constr_of_monomorphic_global gr =
       Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
           str " would forget universes.")
 
-let constr_of_global gr = constr_of_monomorphic_global gr
-
-let constr_of_global_univ = mkRef
-
 let fresh_global_or_constr_instance env = function
   | IsConstr c -> c, ContextSet.empty
   | IsGlobal gr -> fresh_global_instance env gr
@@ -99,34 +90,6 @@ let global_of_constr c =
   | Var id -> VarRef id, Instance.empty
   | _ -> raise Not_found
 
-open Declarations
-
-let type_of_reference env r =
-  match r with
-  | VarRef id -> Environ.named_type id env, ContextSet.empty
-
-  | ConstRef c ->
-     let cb = Environ.lookup_constant c env in
-     let ty = cb.const_type in
-     let auctx = Declareops.constant_polymorphic_context cb in
-     let inst, ctx = fresh_instance auctx in
-     Vars.subst_instance_constr inst ty, ctx
-
-  | IndRef ind ->
-    let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
-    let auctx = Declareops.inductive_polymorphic_context mib in
-    let inst, ctx = fresh_instance auctx in
-    let ty = Inductive.type_of_inductive env (specif, inst) in
-    ty, ctx
-
-  | ConstructRef (ind,_ as cstr) ->
-    let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
-    let auctx = Declareops.inductive_polymorphic_context mib in
-    let inst, ctx = fresh_instance auctx in
-    Inductive.type_of_constructor (cstr,inst) specif, ctx
-
-let type_of_global t = type_of_reference (Global.env ()) t
-
 let fresh_sort_in_family = function
   | InSProp -> Sorts.sprop, ContextSet.empty
   | InProp -> Sorts.prop, ContextSet.empty
@@ -135,11 +98,6 @@ let fresh_sort_in_family = function
     let u = fresh_level () in
       sort_of_univ (Univ.Universe.make u), ContextSet.singleton u
 
-let new_sort_in_family sf =
-  fst (fresh_sort_in_family sf)
-
-let extend_context = Univ.extend_in_context_set
-
 let new_global_univ () =
   let u = fresh_level () in
   (Univ.Universe.make u, ContextSet.singleton u)
diff --git a/engine/univGen.mli b/engine/univGen.mli
index b4598e10d0..34920e5620 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -24,16 +24,7 @@ val new_univ_id : unit -> univ_unique_id (** for the stm *)
 val new_univ_global : unit -> Level.UGlobal.t
 val fresh_level : unit -> Level.t
 
-val new_univ : unit -> Universe.t
-[@@ocaml.deprecated "Use [new_univ_level]"]
-val new_Type : unit -> types
-[@@ocaml.deprecated "Use [new_univ_level]"]
-val new_Type_sort : unit -> Sorts.t
-[@@ocaml.deprecated "Use [new_univ_level]"]
-
 val new_global_univ : unit -> Universe.t in_universe_context_set
-val new_sort_in_family : Sorts.family -> Sorts.t
-[@@ocaml.deprecated "Use [fresh_sort_in_family]"]
 
 (** Build a fresh instance for a given context, its associated substitution and
     the instantiated constraints. *)
@@ -66,27 +57,9 @@ val fresh_universe_context_set_instance : ContextSet.t ->
 (** Raises [Not_found] if not a global reference. *)
 val global_of_constr : constr -> GlobRef.t puniverses
 
-val constr_of_global_univ : GlobRef.t puniverses -> constr
-[@@ocaml.deprecated "Use [Constr.mkRef]"]
-
-val extend_context : 'a in_universe_context_set -> ContextSet.t ->
-  'a in_universe_context_set
-[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
-
 (** Create a fresh global in the global environment, without side effects.
     BEWARE: this raises an error on polymorphic constants/inductives:
     the constraints should be properly added to an evd.
     See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
     the proper way to get a fresh copy of a polymorphic global reference. *)
 val constr_of_monomorphic_global : GlobRef.t -> constr
-
-val constr_of_global : GlobRef.t -> constr
-[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\
-                     use [constr_of_monomorphic_global] if the reference is guaranteed to\
-                     be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"]
-
-(** Returns the type of the global reference, by creating a fresh instance of polymorphic
-    references and computing their instantiated universe context. (side-effect on the
-    universe counter, use with care). *)
-val type_of_global : GlobRef.t -> types in_universe_context_set
-[@@ocaml.deprecated "use [Typeops.type_of_global]"]
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d83a0ce918..90fb5a2036 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -120,8 +120,6 @@ let argument_position_eq p1 p2 = match p1, p2 with
 | Hyp h1, Hyp h2 -> Int.equal h1 h2
 | _ -> false
 
-let explicitation_eq = Constrexpr_ops.explicitation_eq
-
 type implicit_explanation =
   | DepRigid of argument_position
   | DepFlex of argument_position
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 0070423530..ccdd448460 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -143,7 +143,3 @@ val projection_implicits : env -> Projection.t -> implicit_status list ->
 val select_impargs_size : int -> implicits_list list -> implicit_status list
 
 val select_stronger_impargs : implicits_list list -> implicit_status list
-
-val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
-  [@@ocaml.deprecated "Use Constrexpr_ops.explicitation_eq instead (since 8.10)"]
-(** Equality on [explicitation]. *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 009eb3da38..bb3b0a538e 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -49,20 +49,6 @@ let weaker_noccur_between env x nvars t =
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
 
-(* Errors related to inductive constructions *)
-type inductive_error = Type_errors.inductive_error =
-  | NonPos of env * constr * constr
-  | NotEnoughArgs of env * constr * constr
-  | NotConstructor of env * Id.t * constr * constr * int * int
-  | NonPar of env * constr * int * constr * constr
-  | SameNamesTypes of Id.t
-  | SameNamesConstructors of Id.t
-  | SameNamesOverlap of Id.t list
-  | NotAnArity of env * constr
-  | BadEntry
-  | LargeNonPropInductiveNotInType
-  | BadUnivs
-
 exception InductiveError = Type_errors.InductiveError
 
 (************************************************************************)
@@ -84,6 +70,7 @@ exception IllFormedInd of ill_formed_ind
 let mind_extract_params = decompose_prod_n_assum
 
 let explain_ind_err id ntyp env nparamsctxt c err =
+  let open Type_errors in
   let (_lparams,c') = mind_extract_params nparamsctxt c in
   match err with
     | LocalNonPos kt ->
@@ -329,7 +316,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
           | Prod (na,b,d) ->
 	      let () = assert (List.is_empty largs) in
 	      if not recursive && not (noccur_between n ntypes b) then
-	        raise (InductiveError BadEntry);
+                raise (InductiveError Type_errors.BadEntry);
               let nmr',recarg = check_pos ienv nmr b in
               let ienv' = ienv_push_var ienv (na,b,mk_norec) in
                 check_constr_rec ienv' nmr' (recarg::lrec) d
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7810c1723e..1b8e4208ff 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -9,28 +9,9 @@
 (************************************************************************)
 
 open Names
-open Constr
 open Declarations
 open Environ
 open Entries
 
 (** Check an inductive. *)
 val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-
-(** Deprecated *)
-type inductive_error =
-  | NonPos of env * constr * constr
-  | NotEnoughArgs of env * constr * constr
-  | NotConstructor of env * Id.t * constr * constr * int * int
-  | NonPar of env * constr * int * constr * constr
-  | SameNamesTypes of Id.t
-  | SameNamesConstructors of Id.t
-  | SameNamesOverlap of Id.t list
-  | NotAnArity of env * constr
-  | BadEntry
-  | LargeNonPropInductiveNotInType
-  | BadUnivs
-[@@ocaml.deprecated "Use [Type_errors.inductive_error]"]
-
-exception InductiveError of Type_errors.inductive_error
-[@@ocaml.deprecated "Use [Type_errors.InductiveError]"]
diff --git a/kernel/names.ml b/kernel/names.ml
index 9f27212967..047a1d6525 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -376,9 +376,6 @@ module KerName = struct
     { modpath; knlabel; refhash = -1; }
   let repr kn = (kn.modpath, kn.knlabel)
 
-  let make2 = make
-  [@@ocaml.deprecated "Please use [KerName.make]"]
-
   let modpath kn = kn.modpath
   let label kn = kn.knlabel
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 61df3bad0e..2238e932b0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -278,9 +278,6 @@ sig
   val make : ModPath.t -> Label.t -> t
   val repr : t -> ModPath.t * Label.t
 
-  val make2 : ModPath.t -> Label.t -> t
-  [@@ocaml.deprecated "Please use [KerName.make]"]
-
   (** Projections *)
   val modpath : t -> ModPath.t
   val label : t -> Label.t
diff --git a/lib/rtree.ml b/lib/rtree.ml
index e1c6a4c4d6..66d9eba3f7 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -115,8 +115,6 @@ struct
 
 end
 
-let smartmap = Smart.map
-
 (** Structural equality test, parametrized by an equality on elements *)
 
 let rec raw_eq cmp t t' = match t, t' with
@@ -149,9 +147,6 @@ let equiv cmp cmp' =
 let equal cmp t t' =
   t == t' || raw_eq cmp t t' || equiv cmp cmp t t'
 
-(** Deprecated alias *)
-let eq_rtree = equal
-
 (** Intersection of rtrees of same arity *)
 let rec inter cmp interlbl def n histo t t' =
   try
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 5ab14f6039..67519aa387 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -77,15 +77,9 @@ val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -
 (** See also [Smart.map] *)
 val map : ('a -> 'b) -> 'a t -> 'b t
 
-val smartmap : ('a -> 'a) -> 'a t -> 'a t
-(** @deprecated Same as [Smart.map] *)
-
 (** A rather simple minded pretty-printer *)
 val pp_tree : ('a -> Pp.t) -> 'a t -> Pp.t
 
-val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
-(** @deprecated Same as [Rtree.equal] *)
-
 module Smart :
 sig
 
diff --git a/library/global.ml b/library/global.ml
index 55aed1c56e..06e06a8cf2 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -157,11 +157,6 @@ let import c u d = globalize (Safe_typing.import c u d)
 let env_of_context hyps =
   reset_with_named_context hyps (env())
 
-let type_of_global_in_context = Typeops.type_of_global_in_context
-
-let universes_of_global gr = 
-  universes_of_global (env ()) gr
-
 let is_polymorphic r = Environ.is_polymorphic (env()) r
 
 let is_template_polymorphic r = is_template_polymorphic (env ()) r
diff --git a/library/global.mli b/library/global.mli
index 76ac3f6279..a60de48897 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -131,14 +131,6 @@ val is_polymorphic : GlobRef.t -> bool
 val is_template_polymorphic : GlobRef.t -> bool
 val is_type_in_type : GlobRef.t -> bool
 
-val type_of_global_in_context : Environ.env -> 
-  GlobRef.t -> Constr.types * Univ.AUContext.t
-  [@@ocaml.deprecated "alias of [Typeops.type_of_global_in_context]"]
-
-(** Returns the universe context of the global reference (whatever its polymorphic status is). *)
-val universes_of_global : GlobRef.t -> Univ.AUContext.t
-[@@ocaml.deprecated "Use [Environ.universes_of_global]"]
-
 (** {6 Retroknowledge } *)
 
 val register_inline : Constant.t -> unit
diff --git a/library/globnames.ml b/library/globnames.ml
index db2e8bfaed..99dcc43ad1 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -85,15 +85,6 @@ let printable_constr_of_global = function
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
-module RefOrdered = Names.GlobRef.Ordered
-module RefOrdered_env = Names.GlobRef.Ordered_env
-
-module Refmap = Names.GlobRef.Map
-module Refset = Names.GlobRef.Set
-
-module Refmap_env = Names.GlobRef.Map_env
-module Refset_env = Names.GlobRef.Set_env
-
 (* Extended global references *)
 
 type syndef_name = KerName.t
@@ -134,6 +125,3 @@ end
 type global_reference_or_constr = 
   | IsGlobal of global_reference
   | IsConstr of constr
-
-(* Deprecated *)
-let eq_gr = GlobRef.equal
diff --git a/library/globnames.mli b/library/globnames.mli
index d49ed453f5..14e422b743 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -25,8 +25,6 @@ val isConstRef : GlobRef.t -> bool
 val isIndRef : GlobRef.t -> bool
 val isConstructRef : GlobRef.t -> bool
 
-val eq_gr : GlobRef.t -> GlobRef.t -> bool
-[@@ocaml.deprecated "Use Names.GlobRef.equal"]
 val canonical_gr : GlobRef.t -> GlobRef.t
 
 val destVarRef : GlobRef.t -> variable
@@ -48,22 +46,6 @@ val printable_constr_of_global : GlobRef.t -> constr
    raise [Not_found] if not a global reference *)
 val global_of_constr : constr -> GlobRef.t
 
-module RefOrdered = Names.GlobRef.Ordered
-[@@ocaml.deprecated "Use Names.GlobRef.Ordered"]
-
-module RefOrdered_env = Names.GlobRef.Ordered_env
-[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"]
-
-module Refset = Names.GlobRef.Set
-[@@ocaml.deprecated "Use Names.GlobRef.Set"]
-module Refmap = Names.GlobRef.Map
-[@@ocaml.deprecated "Use Names.GlobRef.Map"]
-
-module Refset_env = GlobRef.Set_env
-[@@ocaml.deprecated "Use Names.GlobRef.Set_env"]
-module Refmap_env = GlobRef.Map_env
-[@@ocaml.deprecated "Use Names.GlobRef.Map_env"]
-
 (** {6 Extended global references } *)
 
 type syndef_name = KerName.t
diff --git a/library/lib.ml b/library/lib.ml
index d4381a6923..a046360822 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -278,7 +278,7 @@ let start_mod is_type export id mp fs =
   let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in
   let exists =
     if is_type then Nametab.exists_cci (make_path id)
-    else Nametab.exists_module dir
+    else Nametab.exists_dir dir
   in
   if exists then
     user_err ~hdr:"open_module" (Id.print id ++ str " already exists");
@@ -569,7 +569,7 @@ let open_section id =
   let opp = !lib_state.path_prefix in
   let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
   let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
-  if Nametab.exists_section obj_dir then
+  if Nametab.exists_dir obj_dir then
     user_err ~hdr:"open_section" (Id.print id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:false in
   add_entry (make_foname id) (OpenedSection (prefix, fs));
diff --git a/library/nametab.ml b/library/nametab.ml
index 95890b2edf..bd0ea5f04f 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -43,12 +43,6 @@ module GlobDirRef = struct
 
 end
 
-type global_dir_reference = GlobDirRef.t
-[@@ocaml.deprecated "Use [GlobDirRef.t]"]
-
-let eq_global_dir_reference = GlobDirRef.equal
-[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
-
 exception GlobalizationError of qualid
 
 let error_global_not_found qid =
@@ -516,10 +510,6 @@ let exists_cci sp = ExtRefTab.exists sp !the_ccitab
 
 let exists_dir dir = DirTab.exists dir !the_dirtab
 
-let exists_section = exists_dir
-
-let exists_module = exists_dir
-
 let exists_modtype sp = MPTab.exists sp !the_modtypetab
 
 let exists_universe kn = UnivTab.exists kn !the_univtab
@@ -585,10 +575,3 @@ let global_inductive qid =
   | ref ->
       user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
         (pr_qualid qid ++ spc () ++ str "is not an inductive type")
-
-(********************************************************************)
-
-(* Deprecated synonyms *)
-
-let extended_locate = locate_extended
-let absolute_reference = global_of_path
diff --git a/library/nametab.mli b/library/nametab.mli
index fccb8fd918..a4f177aad0 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -89,13 +89,6 @@ module GlobDirRef : sig
   val equal : t -> t -> bool
 end
 
-type global_dir_reference = GlobDirRef.t
-[@@ocaml.deprecated "Use [GlobDirRef.t]"]
-
-val eq_global_dir_reference :
-  GlobDirRef.t -> GlobDirRef.t -> bool
-[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
-
 exception GlobalizationError of qualid
 
 (** Raises a globalization error *)
@@ -170,10 +163,6 @@ val extended_global_of_path : full_path -> extended_global_reference
 val exists_cci : full_path -> bool
 val exists_modtype : full_path -> bool
 val exists_dir : DirPath.t -> bool
-val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
-
-val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
-
 val exists_universe : full_path -> bool
 
 (** {6 These functions locate qualids into full user names } *)
@@ -220,11 +209,6 @@ val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
 
-(** Deprecated synonyms *)
-
-val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
-val absolute_reference : full_path -> GlobRef.t (** = global_of_path *)
-
 (** {5 Generic name handling} *)
 
 (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3dd3a430e8..1fca132655 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -132,7 +132,7 @@ let nat = function () -> (coq_init_constant "nat")
 let iter_ref () =  
   try find_reference ["Recdef"] "iter" 
   with Not_found -> user_err Pp.(str "module Recdef not loaded")
-let iter_rd = function () -> (constr_of_global (delayed_force iter_ref))
+let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref))
 let eq = function () -> (coq_init_constant "eq")
 let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
 let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
@@ -145,7 +145,7 @@ let coq_O = function () -> (coq_init_constant "O")
 let coq_S = function () -> (coq_init_constant "S")
 let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
 let max_ref = function () -> (find_reference ["Recdef"] "max")
-let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref))
+let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref))
 
 let f_S t = mkApp(delayed_force coq_S, [|t|]);;
 
@@ -1041,13 +1041,13 @@ let compute_terminate_type nb_args func =
   let open Term in
   let open Constr in
   let open CVars in
-  let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in
+  let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_monomorphic_global func)) in
   let rev_args,b = decompose_prod_n nb_args a_arrow_b in
   let left =
     mkApp(delayed_force iter_rd,
 	  Array.of_list
 	    (lift 5 a_arrow_b:: mkRel 3::
-	       constr_of_global func::mkRel 1::
+               constr_of_monomorphic_global func::mkRel 1::
 	       List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
 	    )
 	 )
@@ -1065,7 +1065,7 @@ let compute_terminate_type nb_args func =
 		  delayed_force nat,
                   (mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat,
                            mkArrow cond Sorts.Relevant result))))|])in
-  let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref),
+  let value = mkApp(constr_of_monomorphic_global (Util.delayed_force coq_sig_ref),
 		    [|b;
                       (mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in
   compose_prod rev_args value
@@ -1161,7 +1161,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
     fun g ->
       let sigma = project g in
       let ids = Termops.ids_of_named_context (pf_hyps g) in
-      let func_body = (def_of_const (constr_of_global func)) in
+      let func_body = (def_of_const (constr_of_monomorphic_global func)) in
       let func_body = EConstr.of_constr func_body in
       let (f_name, _, body1) = destLambda sigma func_body in
       let f_id =
@@ -1222,7 +1222,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
 
 let get_current_subgoals_types pstate =
   let p = Proof_global.give_me_the_proof pstate in
-  let sgs,_,_,_,sigma = Proof.proof p in
+  let Proof.{ goals=sgs; sigma; _ } = Proof.data p in
   sigma, List.map (Goal.V82.abstract_type sigma) sgs
 
 exception EmptySubgoals
@@ -1253,7 +1253,7 @@ let build_and_l sigma l =
 	let c,tac,nb = f pl in
 	mk_and p1 c,
 	tclTHENS
-	  (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_global conj_constr))))
+          (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_monomorphic_global conj_constr))))
 	  [tclIDTAC;
 	   tac
 	  ],nb+1
@@ -1437,7 +1437,7 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
   (cont_tactic:Id.t list -> tactic) g =
   let sigma = project g in
   let ids = pf_ids_of_hyps g in
-  let terminate_constr = constr_of_global term_f in
+  let terminate_constr = constr_of_monomorphic_global term_f in
   let terminate_constr = EConstr.of_constr terminate_constr in
   let nargs = nb_prod (project g) (EConstr.of_constr (type_of_const sigma terminate_constr)) in
   let x = n_x_id ids nargs in
@@ -1457,7 +1457,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
 	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
     in
     let evd = Evd.from_ctx uctx in
-    let f_constr = constr_of_global f_ref in
+    let f_constr = constr_of_monomorphic_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd
        (EConstr.of_constr equation_lemma_type) in
@@ -1466,12 +1466,12 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
 	  (fun  x ->
 	     prove_eq (fun _ -> tclIDTAC)
 	       {nb_arg=nb_arg;
-		f_terminate = EConstr.of_constr (constr_of_global terminate_ref); 
+                f_terminate = EConstr.of_constr (constr_of_monomorphic_global terminate_ref);
 	        f_constr = EConstr.of_constr f_constr; 
 		concl_tac = tclIDTAC;
 		func=functional_ref;
 		info=(instantiate_lambda Evd.empty
-	       		(EConstr.of_constr (def_of_const (constr_of_global functional_ref)))
+                        (EConstr.of_constr (def_of_const (constr_of_monomorphic_global functional_ref)))
 	       		(EConstr.of_constr f_constr::List.map mkVar x)
 		);
 		is_main_branch = true;
@@ -1570,9 +1570,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     if not stop
     then
       let eq_ref = Nametab.locate (qualid_of_ident equation_id ) in
-      let f_ref = destConst (constr_of_global f_ref)
-      and functional_ref = destConst (constr_of_global functional_ref)
-      and eq_ref = destConst (constr_of_global eq_ref) in
+      let f_ref = destConst (constr_of_monomorphic_global f_ref)
+      and functional_ref = destConst (constr_of_monomorphic_global functional_ref)
+      and eq_ref = destConst (constr_of_monomorphic_global eq_ref) in
       generate_induction_principle f_ref tcc_lemma_constr
         functional_ref eq_ref rec_arg_num
         (EConstr.of_constr rec_arg_type)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ef6af16036..de9dec0f74 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -207,7 +207,7 @@ struct
     * ZMicromega.v
     *)
 
-  let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n)
+  let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n)
   let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules
   [@@@ocaml.warning "+3"]
 
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index e349031952..93c0d5c236 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -446,7 +446,7 @@ let lz_setoid_relation =
   | Some (env', srel) when env' == env -> srel
   | _ ->
     let srel =
-       try Some (UnivGen.constr_of_global @@
+       try Some (UnivGen.constr_of_monomorphic_global @@
                  Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"])
        with _ -> None in
     last_srel := Some (env, srel); srel
@@ -491,7 +491,7 @@ let rwprocess_rule dir rule gl =
           | _ ->
             let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
             EConstr.mkApp (pi2, ra), sigma in
-        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.True.type"))) then
+        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then
          let s, sigma = sr sigma 2 in
          loop (converse_dir d) sigma s a.(1) rs 0
         else
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 99013a19c9..6b149a8b41 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1769,28 +1769,3 @@ let unify ?flags ?(with_ho=true) env evd cv_pb ty1 ty2 =
      solve_unif_constraints_with_heuristics ~flags ~with_ho env evd
   | UnifFailure (evd, reason) ->
      raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason)))
-
-(* deprecated *)
-let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd =
-  let flags = default_flags_of ts in
-  match evar_conv_x flags env evd CONV  t1 t2 with
-  | Success evd' -> evd'
-  | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
-
-let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd =
-  let flags = default_flags_of ts in
-  match evar_conv_x flags env evd CUMUL t1 t2 with
-  | Success evd' -> evd'
-  | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
-
-let make_opt = function
-  | Success evd -> Some evd
-  | UnifFailure _ -> None
-
-let conv env ?(ts=default_transparent_state env) evd t1 t2 =
-  let flags = default_flags_of ts in
-  make_opt(evar_conv_x flags env evd CONV t1 t2)
-
-let cumul env ?(ts=default_transparent_state env) evd t1 t2 =
-  let flags = default_flags_of ts in
-  make_opt(evar_conv_x flags env evd CUMUL t1 t2)
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index bf83f5e88f..eae961714d 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -46,19 +46,6 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error
 val unify_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
 val unify_leq_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
 
-(** returns exception UnableToUnify with best known evar_map if not unifiable *)
-val the_conv_x     : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
-[@@ocaml.deprecated "Use Evarconv.unify_delay instead"]
-val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
-[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"]
-(** The same function resolving evars by side-effect and
-   catching the exception *)
-
-val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
-[@@ocaml.deprecated "Use Evarconv.unify_delay instead"]
-val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
-[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"]
-
 (** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining
     constraints. In case of success the two terms are unified without condition.
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index f4986652b3..bd97104f60 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -63,7 +63,7 @@ let keyword s = tag_keyword (str s)
 let get_new_id locals id =
   let rec get_id l id =
     let dir = DirPath.make [id] in
-      if not (Nametab.exists_module dir) then
+      if not (Nametab.exists_dir dir) then
 	id
       else
 	get_id (Id.Set.add id l) (Namegen.next_ident_away id l)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 978b1f6f78..778d98b2cd 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -126,9 +126,6 @@ type t =
   (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
   }
 
-let initial_goals pf = Proofview.initial_goals pf.entry
-let initial_euctx pf = pf.initial_euctx
-
 (*** General proof functions ***)
 
 let proof p =
@@ -147,33 +144,6 @@ let proof p =
   let given_up = p.given_up in
   (goals,stack,shelf,given_up,sigma)
 
-type 'a pre_goals = {
-  fg_goals : 'a list;
-  (** List of the focussed goals *)
-  bg_goals : ('a list * 'a list) list;
-  (** Zipper representing the unfocussed background goals *)
-  shelved_goals : 'a list;
-  (** List of the goals on the shelf. *)
-  given_up_goals : 'a list;
-  (** List of the goals that have been given up *)
-}
-
-let map_structured_proof pfts process_goal: 'a pre_goals =
-  let (goals, zipper, shelf, given_up, sigma) = proof pfts in
-  let fg = List.map (process_goal sigma) goals in
-  let map_zip (lg, rg) =
-    let lg = List.map (process_goal sigma) lg in
-    let rg = List.map (process_goal sigma) rg in
-    (lg, rg)
-  in
-  let bg = List.map map_zip zipper in
-  let shelf = List.map (process_goal sigma) shelf in
-  let given_up = List.map (process_goal sigma) given_up in
-    { fg_goals = fg;
-      bg_goals = bg;
-      shelved_goals = shelf;
-      given_up_goals = given_up; }
-
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
   | [] -> pv
@@ -441,22 +411,6 @@ let in_proof p k = k (Proofview.return p.proofview)
 let unshelve p =
   { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] }
 
-let pr_proof p =
-  let p = map_structured_proof p (fun _sigma g -> g) in
-  Pp.(
-    let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
-    let rec aux acc = function
-      | [] -> acc
-      | (before,after)::stack ->
-         aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++
-              pr_goal_list after) stack in
-    str "[" ++ str "focus structure: " ++
-               aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++
-    str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++
-    str "given up: " ++ pr_goal_list p.given_up_goals ++
-    str "]"
-  )
-
 (*** Compatibility layer with <=v8.2 ***)
 module V82 = struct
 
@@ -554,3 +508,19 @@ let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name;
   let stack =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in
   { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly }
+
+let pr_proof p =
+  let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in
+  Pp.(
+    let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
+    let rec aux acc = function
+      | [] -> acc
+      | (before,after)::stack ->
+         aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++
+              pr_goal_list after) stack in
+    str "[" ++ str "focus structure: " ++
+               aux (pr_goal_list fg_goals) bg_goals ++ str ";" ++ spc () ++
+    str "shelved: " ++ pr_goal_list shelf ++ str ";" ++ spc () ++
+    str "given up: " ++ pr_goal_list given_up ++
+    str "]"
+  )
diff --git a/proofs/proof.mli b/proofs/proof.mli
index defef57a8d..1f4748141a 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -34,30 +34,6 @@
 (* Type of a proof. *)
 type t
 
-(* Returns a stylised view of a proof for use by, for instance,
-   ide-s. *)
-(* spiwack: the type of [proof] will change as we push more refined
-   functions to ide-s. This would be better than spawning a new nearly
-   identical function everytime. Hence the generic name. *)
-(* In this version: returns the focused goals, a representation of the
-   focus stack (the goals at each level), a representation of the
-   shelf (the list of goals on the shelf), a representation of the
-   given up goals (the list of the given up goals) and the underlying
-   evar_map *)
-val proof : t ->
-  Goal.goal list
-  * (Goal.goal list * Goal.goal list) list
-  * Goal.goal list
-  * Goal.goal list
-  * Evd.evar_map
-[@@ocaml.deprecated "use [Proof.data]"]
-
-val initial_goals : t -> (EConstr.constr * EConstr.types) list
-[@@ocaml.deprecated "use [Proof.data]"]
-
-val initial_euctx : t -> UState.t
-[@@ocaml.deprecated "use [Proof.data]"]
-
 type data =
   { sigma : Evd.evar_map
   (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *)
@@ -81,29 +57,6 @@ type data =
 
 val data : t -> data
 
-(* Generic records structured like the return type of proof *)
-type 'a pre_goals = {
-  fg_goals : 'a list;
-  [@ocaml.deprecated "use [Proof.data]"]
-  (** List of the focussed goals *)
-  bg_goals : ('a list * 'a list) list;
-  [@ocaml.deprecated "use [Proof.data]"]
-  (** Zipper representing the unfocussed background goals *)
-  shelved_goals : 'a list;
-  [@ocaml.deprecated "use [Proof.data]"]
-  (** List of the goals on the shelf. *)
-  given_up_goals : 'a list;
-  [@ocaml.deprecated "use [Proof.data]"]
-  (** List of the goals that have been given up *)
-}
-[@@ocaml.deprecated "use [Proof.data]"]
-
-(* needed in OCaml 4.05.0, not needed in newer ones *)
-[@@@ocaml.warning "-3"]
-val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"]
-[@@ocaml.deprecated "use [Proof.data]"]
-[@@@ocaml.warning "+3"]
-
 (*** General proof functions ***)
 val start
   :  name:Names.Id.t
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 7b3d9e534b..93031c2202 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -104,10 +104,6 @@ let db_pr_goal sigma g =
 let pr_gls gls =
   hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
 
-let pr_glls glls =
-  hov 0 (pr_evar_map (Some 2) (Global.env()) (sig_sig glls) ++ fnl () ++
-         prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls))
-
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New = struct
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 218011c316..23e1e6f566 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -68,8 +68,6 @@ val pf_conv_x_leq  : Goal.goal sigma -> constr -> constr -> bool
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : Goal.goal sigma -> Pp.t
-val pr_glls   : Goal.goal list sigma -> Pp.t
-[@@ocaml.deprecated "Please move to \"new\" proof engine"]
 
 (** Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
diff --git a/tactics/ppred.mli b/tactics/ppred.mli
index be21236f4e..c68fab5296 100644
--- a/tactics/ppred.mli
+++ b/tactics/ppred.mli
@@ -6,11 +6,6 @@ val pr_with_occurrences :
 val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
 val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
 
-val pr_red_expr :
-  ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
-  (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t
-  [@@ocaml.deprecated "Use pr_red_expr_env instead"]
-
 val pr_red_expr_env : Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
   (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 9a18baa0bc..ec43dbb1d7 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -184,10 +184,6 @@ let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
          (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
 
-let warn_deprecated_boot =
-  CWarnings.create ~name:"deprecated-boot" ~category:"noop"
-         (fun () -> Pp.strbrk "The -boot option is deprecated, please use -q and/or -coqlib options instead.")
-
 let set_inputstate opts s =
   warn_deprecated_inputstate ();
   { opts with inputstate = Some s }
@@ -488,9 +484,6 @@ let parse_args ~help ~init arglist : t * string list =
       { oval with batch = true }
     |"-test-mode" -> Vernacentries.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
-    |"-boot" ->
-      warn_deprecated_boot ();
-      { oval with load_rcfile = false; }
     |"-bt" -> Backtrace.record_backtrace true; oval
     |"-color" -> set_color oval (next ())
     |"-config"|"--config" -> { oval with print_config = true }
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9323a57417..b769405cf6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -271,31 +271,6 @@ let init_toploop opts =
   let state = { doc; sid; proof = None; time = opts.time } in
   Ccompile.load_init_vernaculars opts ~state, opts
 
-(* To remove in 8.11 *)
-let call_coqc args =
-  let remove str arr = Array.(of_list List.(filter (fun l -> not String.(equal l str)) (to_list arr))) in
-  let coqc_name = Filename.remove_extension (System.get_toplevel_path "coqc") in
-  let args = remove "-compile" args in
-  Unix.execv coqc_name args
-
-let deprecated_coqc_warning = CWarnings.(create
-    ~name:"deprecate-compile-arg"
-    ~category:"toplevel"
-    ~default:Enabled
-    (fun opt_name -> Pp.(seq [str "The option "; str opt_name; str" is deprecated, please use coqc."])))
-
-let rec coqc_deprecated_check args acc extras =
-  match extras with
-  | [] -> acc
-  | "-o" :: _ :: rem ->
-    deprecated_coqc_warning "-o";
-    coqc_deprecated_check args acc rem
-  | ("-compile"|"-compile-verbose") :: file :: rem ->
-    deprecated_coqc_warning "-compile";
-    call_coqc args
-  | x :: rem ->
-    coqc_deprecated_check args (x::acc) rem
-
 let coqtop_init ~opts extra =
   init_color opts;
   CoqworkmgrApi.(init !async_proofs_worker_priority);
@@ -317,7 +292,6 @@ let start_coq custom =
         init_toplevel
           ~help:Usage.print_usage_coqtop ~init:default custom.init
           (List.tl (Array.to_list Sys.argv)) in
-      let extras = coqc_deprecated_check Sys.argv [] extras in
       if not (CList.is_empty extras) then begin
         prerr_endline ("Don't know what to do with "^String.concat " " extras);
         prerr_endline "See -help for the list of supported options";
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 7074215afe..da2094653b 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -102,12 +102,6 @@ let print_usage_coqtop () =
 coqtop specific options:\
 \n\
 \n  -batch                 batch mode (exits just after argument parsing)\
-\n\
-\nDeprecated options [use coqc instead]:\
-\n\
-\n  -compile f.v           compile Coq file f.v (implies -batch)\
-\n  -compile-verbose f.v   verbosely compile Coq file f.v (implies -batch)\
-\n  -o f.vo                use f.vo as the output file name\
 \n";
   flush stderr ;
   exit 1
@@ -128,14 +122,6 @@ coqc specific options:\
 \nUndocumented:\
 \n  -vio2vo                [see manual]\
 \n  -check-vio-tasks       [see manual]\
-\n\
-\nDeprecated options:\
-\n\
-\n  -image f               specify an alternative executable for Coq\
-\n  -opt                   run the native-code version of Coq\
-\n  -byte                  run the bytecode version of Coq\
-\n  -t                     keep temporary files\
-\n  -outputstate file      save summary state in file \
 \n";
   flush stderr ;
   exit 1
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index f58eeae6dc..b2382ce6fc 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1348,9 +1348,6 @@ let explain_pattern_matching_error env sigma = function
   | CannotInferPredicate typs ->
       explain_cannot_infer_predicate env sigma typs
 
-let map_pguard_error = map_pguard_error
-let map_ptype_error = map_ptype_error
-
 let explain_reduction_tactic_error = function
   | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
       let e = map_ptype_error EConstr.of_constr e in
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index d0f42ea16b..d1c1c092e3 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -43,9 +43,4 @@ val explain_module_error : Modops.module_typing_error -> Pp.t
 val explain_module_internalization_error :
   Modintern.module_internalization_error -> Pp.t
 
-val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
-[@@ocaml.deprecated "Use [Type_errors.map_pguard_error]."]
-val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
-[@@ocaml.deprecated "Use [Type_errors.map_ptype_error]."]
-
 val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t