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.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/type_errors.mli')

diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 613ccb78ca..3e954d6a8e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -82,6 +82,7 @@ type inductive_error =
   | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
+  | BadUnivs
 
 exception InductiveError of inductive_error
 
-- 
cgit v1.2.3