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.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/type_errors.mli')

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