diff options
| author | Gaëtan Gilbert | 2019-01-03 16:59:58 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:15 +0100 |
| commit | 5cb337a0862e06a5b103b00c43cf9777e3468923 (patch) | |
| tree | ceb750d06d159cf59d51ca71af152de1af5bc466 /kernel/type_errors.mli | |
| parent | 23f84f37c674a07e925925b7e0d50d7ee8414093 (diff) | |
Inductives in SProp, forbid primitive records with only sprop fields
For nonsquashed:
Either
- 0 constructors
- primitive record
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 41a5f19e78..88165a4f07 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -34,6 +34,7 @@ type 'constr pguard_error = | RecCallInCasePred of 'constr | NotGuardedForm of 'constr | ReturnPredicateNotCoInductive of 'constr + | FixpointOnIrrelevantInductive type guard_error = constr pguard_error |