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.

---
 toplevel/himsg.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 16d3240294..a0a3d947ed 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -425,6 +425,10 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
       str "Sub-expression " ++ pr_lconstr_env env c ++
       strbrk " not in guarded form (should be a constructor," ++
       strbrk " an abstraction, a match, a cofix or a recursive call)"
+  | ReturnPredicateNotCoInductive c ->
+     str "The return clause of the following pattern matching should be" ++
+     strbrk "a coinductive type:" ++
+     spc () ++ pr_lconstr_env env c
   in
   prt_name i ++ str " is ill-formed." ++ fnl () ++
   pr_ne_context_of (str "In environment") env ++
-- 
cgit v1.2.3