test-suite/bugs/closed/4616.v


1
2
3
4
5
6
7

Require Coq.extraction.Extraction.

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