aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2319.v
blob: e06fb97590879552d9a3fec9e9a2098992c02451 (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.