When I extract the following Coq data types to OCaml:
Inductive Foo := | A | B.
Inductive Bar (f:Foo) := | C | D.
Extraction Language Ocaml.
Extraction "test.ml" Foo Bar.
I get the following ML code:
type foo =
| A
| B
type bar =
| C
| D
The 'bar' type is different from Coq's as it does have 'f' as a part of its type signature.
What is the best way to define such types so they are extracted well to OCaml?