diff options
Diffstat (limited to 'kernel/type_errors.mli')
| -rw-r--r-- | kernel/type_errors.mli | 12 |
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 |