Merge PR #11478: Nicer kernel universe error for inductives

Reviewed-by: ppedrot

1 files changed, 7 insertions, 5 deletions

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