From 65816f94ba427edf8999bf42633d0aad064e8ce4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 5 Jan 2017 19:54:41 +0100
Subject: Fixing a little bug in printing cofix with no arguments.

---
 test-suite/output/Fixpoint.out | 2 ++
 test-suite/output/Fixpoint.v   | 5 ++++-
 2 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index a13ae4624a..6879cbc3c2 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -10,3 +10,5 @@ let fix f (m : nat) : nat := match m with
                              end in f 0
      : nat
 Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1)
+     = cofix inf : Inf := {| projS := inf |}
+     : Inf
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 8afa50ba57..fafb478bad 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,4 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
   omega.
 Qed.
 
-
+CoInductive Inf := S { projS : Inf }.
+Definition expand_Inf (x : Inf) := S (projS x).
+CoFixpoint inf := S inf.
+Eval compute in inf.
-- 
cgit v1.2.3