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

---
 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 09310b42b2..37370377d4 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -31,6 +31,7 @@ type guard_error =
   | RecCallInCaseArg of constr
   | RecCallInCasePred of constr
   | NotGuardedForm of constr
+  | ReturnPredicateNotCoInductive of constr
 
 type arity_error =
   | NonInformativeToInformative
-- 
cgit v1.2.3