Move inductive_error to Type_errors

9 files changed, 53 insertions, 22 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 167258f8bb..d97ab5409e 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -297,7 +297,7 @@ let explain_exn = function
       | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
       | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
 
-  | Indtypes.InductiveError e ->
+  | InductiveError e ->
       hov 0 (str "Error related to inductive types")
 (*      let ctx = Check.get_env() in
       hov 0
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
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 25a4804743..92b1ff7572 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -24,7 +24,7 @@ open Constrexpr_ops
 open Constrintern
 open Impargs
 open Reductionops
-open Indtypes
+open Type_errors
 open Pretyping
 open Indschemes
 open Context.Rel.Declaration
@@ -304,7 +304,7 @@ let inductive_levels env evd poly arities inds =
         let evd =
           if Sorts.is_set du then
             if not (Evd.check_leq evd cu Univ.type0_univ) then
-              raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType)
+              raise (InductiveError LargeNonPropInductiveNotInType)
             else evd
           else evd
             (* Evd.set_leq_sort env evd (Type cu) du *)
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index e1496e58d7..71770a21ca 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -10,7 +10,6 @@
 
 open Pp
 open CErrors
-open Indtypes
 open Type_errors
 open Pretype_errors
 open Indrec
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index f3e1e1fc49..98c8c21699 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -15,7 +15,6 @@ open Nameops
 open Namegen
 open Constr
 open Termops
-open Indtypes
 open Environ
 open Pretype_errors
 open Type_errors
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index bab66b2af4..986906d303 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Indtypes
 open Environ
 open Type_errors
 open Pretype_errors