aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1568.v
blob: 3609e9c83ba63c46351716b98e2f22f650772dfb (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
CoInductive A: Set :=
  mk_A: B -> A
with B: Set :=
  mk_B: A -> B.

CoFixpoint a:A := mk_A b
with b:B := mk_B a.

Goal b = match a with mk_A a1 => a1 end.
  simpl. reflexivity.
Qed.