4 files changed, 2 insertions, 40 deletions
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