test-suite/bugs/closed/bug_5617.v


1
2
3
4
5
6
7
8

Set Primitive Projections.
Record T X := { F : X }.

Fixpoint f (n : nat) : nat :=
match n with
| 0 => 0
| S m => F _ {| F := f |} m
end.