blob: 73d95e91a10682e54a1ba18eac8969535c4e3018 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
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.
|