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/inductive.ml    | 5 +++++
 kernel/type_errors.ml  | 1 +
 kernel/type_errors.mli | 1 +
 3 files changed, 7 insertions(+)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9cfa5c632e..eae4c098d8 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1171,6 +1171,8 @@ let check_one_cofix env nbfix def deftype =
 	      raise (CoFixGuardError (env,UnguardedRecursiveCall c))
 
 	| Case (_,p,tm,vrest) ->
+	   begin
+	   try let _ = codomain_is_coind env p in
             if (noccur_with_meta n nbfix p) then
               if (noccur_with_meta n nbfix tm) then
 		if (List.for_all (noccur_with_meta n nbfix) args) then
@@ -1181,6 +1183,9 @@ let check_one_cofix env nbfix def deftype =
 		raise (CoFixGuardError (env,RecCallInCaseArg c))
             else
 	      raise (CoFixGuardError (env,RecCallInCasePred c))
+	   with CoFixGuardError _ ->
+		raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c))
+	   end
 
 	| Meta _ -> ()
         | Evar _ ->
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 30dcbafe6b..d0ecf9e9ba 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
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