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 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/inductive.ml')

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