Inductives in SProp, forbid primitive records with only sprop fields

For nonsquashed:
Either
- 0 constructors
- primitive record

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