From 5f9a6c17b4353024e7510977a41cfb1de93a0f5f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 10 Jan 2019 14:43:56 +0100
Subject: Move inductive_error to Type_errors

---
 kernel/type_errors.mli | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'kernel/type_errors.mli')

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
-- 
cgit v1.2.3