From b828495753da8f1685e7ca5b6897a580e7bd3f09 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Mon, 21 Apr 2014 00:18:55 -0400
Subject: First attempt at a fix for guard condition on cofixpoints.

---
 kernel/type_errors.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/type_errors.ml')

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 30dcbafe6..d0ecf9e9b 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -30,6 +30,7 @@ type guard_error =
   | RecCallInCaseArg of constr
   | RecCallInCasePred of constr
   | NotGuardedForm of constr
+  | ReturnPredicateNotCoInductive of constr
 
 type arity_error =
   | NonInformativeToInformative
-- 
cgit v1.2.3