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.mli | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'kernel/type_errors.mli')

diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index ae6fd31762..0f29717f12 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -11,6 +11,7 @@
 open Names
 open Constr
 open Environ
+open Univ
 
 (** Type errors. {% \label{typeerrors} %} *)
 
@@ -64,8 +65,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
 
@@ -86,7 +87,8 @@ type inductive_error =
   | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
-  | BadUnivs
+  | MissingConstraints of (Universe.Set.t * Universe.t)
+  (* each universe in the set should have been <= the other one *)
 
 exception InductiveError of inductive_error
 
@@ -133,9 +135,9 @@ val error_ill_typed_rec_body  :
 
 val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
 
-val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
+val error_unsatisfied_constraints : env -> Constraint.t -> 'a
 
-val error_undeclared_universe : env -> Univ.Level.t -> 'a
+val error_undeclared_universe : env -> Level.t -> 'a
 
 val error_disallowed_sprop : env -> 'a
 
-- 
cgit v1.2.3