test-suite/bugs/closed/4616.v


1
2
3
4
5
6

Require Coq.extraction.Extraction.

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