diff options
| author | Gaëtan Gilbert | 2020-01-29 16:36:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-29 16:52:19 +0100 |
| commit | f86fd4b52a29e2ef63f03cc67c845f1fa05aae13 (patch) | |
| tree | 8eed7cda2bb37ac825474e19c1048d1d68d24b5a /kernel/type_errors.ml | |
| parent | 8c04d108e1f57d0e8e11483a7c9de721ab2f026a (diff) | |
Nicer kernel universe error for inductives
Not sure if it's possible to see it without a plugin.
Diffstat (limited to 'kernel/type_errors.ml')
| -rw-r--r-- | kernel/type_errors.ml | 7 |
1 files changed, 4 insertions, 3 deletions
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 |