path: root/test-suite/bugs/closed/4616.v

Set Primitive Projections.
Record Foo' := Foo { foo : Type }.
Axiom f : forall t : Foo', foo t.
Extraction f.