Move inductive_error to Type_errors

4 files changed, 50 insertions, 16 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 68d44f8782..e0f60a3731 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -56,7 +56,7 @@ let is_constructor_head t =
 (* Various well-formedness check for inductive declarations            *)
 
 (* Errors related to inductive constructions *)
-type inductive_error =
+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
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 840e23ed69..b4879611a3 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -19,21 +19,6 @@ open Entries
 (** The different kinds of errors that may result of a malformed inductive
   definition. *)
 
-(** Errors related to inductive constructions *)
-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
-
-exception InductiveError of inductive_error
-
 val infos_and_sort : env -> constr -> Univ.Universe.t
 
 val check_subtyping_arity_constructor : env -> (constr -> constr) -> types -> int -> bool -> unit
@@ -50,3 +35,20 @@ val check_positivity : chkpos:bool ->
 (** The following function does checks on inductive declarations. *)
 
 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
+[@@ocaml.deprecated "Use [Type_errors.inductive_error]"]
+
+exception InductiveError of Type_errors.inductive_error
+[@@ocaml.deprecated "Use [Type_errors.InductiveError]"]
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 60293fe864..9289225eb6 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -68,6 +68,20 @@ type type_error = (constr, types) ptype_error
 
 exception TypeError of env * type_error
 
+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
+
+exception InductiveError of inductive_error
+
 let nfj env {uj_val=c;uj_type=ct} =
   {uj_val=c;uj_type=nf_betaiota env ct}
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 3fd40a7f42..613ccb78ca 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -69,6 +69,24 @@ type type_error = (constr, types) ptype_error
 
 exception TypeError of env * type_error
 
+(** The different kinds of errors that may result of a malformed inductive
+    definition. *)
+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
+
+exception InductiveError of inductive_error
+
+(** Raising functions *)
+
 val error_unbound_rel : env -> int -> 'a
 
 val error_unbound_var : env -> variable -> 'a