blob: fdc8501099a8c3595e83b5800d69c57950e9350b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Set Primitive Projections.
Record Foo' := Foo { foo : nat }.
Extraction foo.
Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }.
Extraction Language Ocaml.
Extraction foo2p.
Definition bla (x : Foo2 0) := foo2p _ x.
Extraction bla.
Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x.
Extraction bla'.
|
