diff options
author | 2017-01-05 19:54:41 +0100 | |
---|---|---|
committer | 2017-01-05 20:13:00 +0100 | |
commit | 65816f94ba427edf8999bf42633d0aad064e8ce4 (patch) | |
tree | 80c9b34a1c2ba5af338a1409473475c5af277890 /test-suite/output/Fixpoint.v | |
parent | 63ca4aac83ced14b9b8065ef43e29f7c2dfd331c (diff) |
Fixing a little bug in printing cofix with no arguments.
Diffstat (limited to 'test-suite/output/Fixpoint.v')
-rw-r--r-- | test-suite/output/Fixpoint.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 8afa50ba5..fafb478ba 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. |