diff options
Diffstat (limited to 'test-suite/output/Fixpoint.out')
| -rw-r--r-- | test-suite/output/Fixpoint.out | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index a13ae462..6879cbc3 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 |