From 5cb337a0862e06a5b103b00c43cf9777e3468923 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 3 Jan 2019 16:59:58 +0100
Subject: Inductives in SProp, forbid primitive records with only sprop fields

For nonsquashed:
Either
- 0 constructors
- primitive record
---
 kernel/type_errors.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/type_errors.ml')

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
-- 
cgit v1.2.3