1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2319.v b/test-suite/bugs/closed/2319.v
new file mode 100644
index 00000000..e06fb975
--- /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