diff options
Diffstat (limited to 'kernel/type_errors.ml')
| -rw-r--r-- | kernel/type_errors.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 9168c32f0e..c45fe1cf00 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -33,6 +33,7 @@ type 'constr pguard_error = | RecCallInCasePred of 'constr | NotGuardedForm of 'constr | ReturnPredicateNotCoInductive of 'constr + | FixpointOnIrrelevantInductive type guard_error = constr pguard_error @@ -173,6 +174,7 @@ let map_pguard_error f = function | RecCallInCasePred c -> RecCallInCasePred (f c) | NotGuardedForm c -> NotGuardedForm (f c) | ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c) +| FixpointOnIrrelevantInductive -> FixpointOnIrrelevantInductive let map_ptype_error f = function | UnboundRel n -> UnboundRel n |