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.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'kernel/type_errors.ml')

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


From 9c678306157b2c6199091709ef7bb067f724f80c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 19 Nov 2018 18:18:26 +0100
Subject: Refactor typechecking of inductive types

We split into smaller functions, use more specific types for universe
manipulation, and try to limit how much of the big tuple gets passed
to subroutines.
---
 kernel/type_errors.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/type_errors.ml')

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 9289225eb6..fd050085d7 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -79,6 +79,7 @@ type inductive_error =
   | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
+  | BadUnivs
 
 exception InductiveError of inductive_error
 
-- 
cgit v1.2.3