From 30d42837c0ae46aa563761ba20e481f7199d6652 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 9 Apr 2014 17:42:32 -0400
Subject: Add another critical bug to the test-suite.

I have a fix, I'm reviewing it because there may be other bugs around.
---
 test-suite/failure/cofixpoint.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/failure/cofixpoint.v

diff --git a/test-suite/failure/cofixpoint.v b/test-suite/failure/cofixpoint.v
new file mode 100644
index 0000000000..cb39893f47
--- /dev/null
+++ b/test-suite/failure/cofixpoint.v
@@ -0,0 +1,15 @@
+(* A bug in the guard checking of nested cofixpoints. *)
+(* Posted by Maxime Dénès on coqdev (Apr 9, 2014).    *)
+
+CoInductive CoFalse := .
+
+CoInductive CoTrue := I.
+
+Fail CoFixpoint loop : CoFalse :=
+  (cofix f := loop with g := loop for f).
+
+Fail CoFixpoint loop : CoFalse :=
+  (cofix f := I with g := loop for g).
+
+Fail CoFixpoint loop : CoFalse :=
+  (cofix f := loop with g := I for f).
\ No newline at end of file
-- 
cgit v1.2.3