Extract Constant foo => "(fun x -> x.foo)".
Extract Constant bar => "(fun x -> x.bar)".
This means that you can create new terms of type [t] in Coq, but you
cannot pattern match against it.
Also, inlined records, that type of the form
type u = U of { foo : bar }
are still not supported, and might never be supported due to the
restriction of OCaml regarding these types (embodied by the error
message “This form is not allowed as the type of the inlined record
could escape”).
With this patch, coqffi will generate equivalent-up-to-extraction type in Coq for OCaml records when the `transparent-types' is enabled.
More precisely, for a record of the form
coqffi will generate the following Coq record
Besides, it will generates the following extraction commands
One for the inductive type
Extract Inductive t => "M.t" [ "(fun (foo,bar) -> { foo;bar }) "].
One per fields
Extract Constant foo => "(fun x -> x.foo)". Extract Constant bar => "(fun x -> x.bar)".
This means that you can create new terms of type [t] in Coq, but you cannot pattern match against it.
Also, inlined records, that type of the form
are still not supported, and might never be supported due to the restriction of OCaml regarding these types (embodied by the error message “This form is not allowed as the type of the inlined record could escape”).