diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-01-23 17:16:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-01-23 17:16:23 +0100 |
| commit | cfce4732363c7a93ffb7231335463d41c47074ea (patch) | |
| tree | 0aa35e11b13dddcfd0fd7029f02e72d8e7df5c0c /test-suite/output | |
| parent | e91ae93106b6bd6d92ef53ac18b04654485a8106 (diff) | |
| parent | a6f687852c0c7509a06fdf16c0af29129b3566d5 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Fixpoint.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Fixpoint.v | 5 |
2 files changed, 6 insertions, 1 deletions
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index a13ae4624..6879cbc3c 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 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. |