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 fae63666c1..23fed99f3e 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -30,6 +30,7 @@ type type_error = * typed_type array | NotInductive of constr | MLCase of string * constr * constr * constr * constr + | CantFindCaseType of constr exception TypeError of path_kind * context * type_error |