Merge PR #9027: Refactor checking of inductive types

Ack-by: SkySkimmer
Reviewed-by: mattam82
Ack-by: maximedenes
Ack-by: ppedrot

1 files changed, 7 insertions, 23 deletions

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 840e23ed69..7810c1723e 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -14,12 +14,10 @@ open Declarations
 open Environ
 open Entries
 
-(** Inductive type checking and errors *)
-
-(** The different kinds of errors that may result of a malformed inductive
-  definition. *)
+(** Check an inductive. *)
+val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
 
-(** Errors related to inductive constructions *)
+(** Deprecated *)
 type inductive_error =
   | NonPos of env * constr * constr
   | NotEnoughArgs of env * constr * constr
@@ -31,22 +29,8 @@ type inductive_error =
   | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
+  | BadUnivs
+[@@ocaml.deprecated "Use [Type_errors.inductive_error]"]
 
-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
-
-val check_positivity : chkpos:bool ->
-           Names.MutInd.t ->
-           Environ.env ->
-           (Constr.constr, Constr.types) Context.Rel.pt ->
-           Declarations.recursivity_kind ->
-           ('a * Names.Id.t list * Constr.types array *
-            (('b, 'c) Context.Rel.pt * 'd))
-           array -> Int.t * Declarations.recarg Rtree.t array
-
-(** The following function does checks on inductive declarations. *)
-
-val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
+exception InductiveError of Type_errors.inductive_error
+[@@ocaml.deprecated "Use [Type_errors.InductiveError]"]