Merge PR #9027: Refactor checking of inductive types

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

1 files changed, 15 insertions, 0 deletions

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 60293fe864..fd050085d7 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -68,6 +68,21 @@ 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
+  | BadUnivs
+
+exception InductiveError of inductive_error
+
 let nfj env {uj_val=c;uj_type=ct} =
   {uj_val=c;uj_type=nf_betaiota env ct}