diff options
| author | Gaëtan Gilbert | 2018-11-19 18:18:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-21 13:22:47 +0100 |
| commit | 9c678306157b2c6199091709ef7bb067f724f80c (patch) | |
| tree | 28bbb08c4500676b2eca478323243d867cf27c15 /kernel/type_errors.mli | |
| parent | 70ce3e98991a96f9d7f181a4a6f5b250457f1245 (diff) | |
Refactor typechecking of inductive types
We split into smaller functions, use more specific types for universe
manipulation, and try to limit how much of the big tuple gets passed
to subroutines.
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 |