From 8529f861ab504e7f891d7b9b3f4ad5aa2c09710a Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 28 Jul 2010 11:00:17 +0000
Subject: fixed bug #2139: compiled cofix loops, missing offset to evaluate
 cofix bodies

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13337 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/2319.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/2319.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2319.v b/test-suite/bugs/closed/2319.v
new file mode 100644
index 0000000000..e06fb97590
--- /dev/null
+++ b/test-suite/bugs/closed/2319.v
@@ -0,0 +1,13 @@
+Section S.
+
+  CoInductive A (X: Type) := mkA: A X -> A X.
+  Variable T : Type.
+
+  (* This used to loop (bug #2319) *)
+  Timeout 5 Eval vm_compute in cofix s : A T := mkA T s.
+
+  CoFixpoint s : A T := mkA T s
+        with t : A unit := mkA unit (mkA unit t).
+  Timeout 5 Eval vm_compute in s.
+
+End S.
\ No newline at end of file
-- 
cgit v1.2.3