diff options
Diffstat (limited to 'kernel/type_errors.mli')
| -rw-r--r-- | kernel/type_errors.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 613ccb78ca..3e954d6a8e 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -82,6 +82,7 @@ type inductive_error = | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType + | BadUnivs exception InductiveError of inductive_error |