From f86fd4b52a29e2ef63f03cc67c845f1fa05aae13 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 29 Jan 2020 16:36:02 +0100
Subject: Nicer kernel universe error for inductives

Not sure if it's possible to see it without a plugin.
---
 kernel/type_errors.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel/type_errors.ml')

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f221ac7a4f..c2cdf98ee8 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -12,6 +12,7 @@ open Names
 open Constr
 open Environ
 open Reduction
+open Univ
 
 (* Type errors. *)
 
@@ -63,8 +64,8 @@ type ('constr, 'types) ptype_error =
   | IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
   | IllTypedRecBody of
       int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
-  | UnsatisfiedConstraints of Univ.Constraint.t
-  | UndeclaredUniverse of Univ.Level.t
+  | UnsatisfiedConstraints of Constraint.t
+  | UndeclaredUniverse of Level.t
   | DisallowedSProp
   | BadRelevance
 
@@ -83,7 +84,7 @@ type inductive_error =
   | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
-  | BadUnivs
+  | MissingConstraints of (Universe.Set.t * Universe.t)
 
 exception InductiveError of inductive_error
 
-- 
cgit v1.2.3