Hi, Thanks for the documentation and the helpful example.
Is there support for extraction? e.g. to see Coq as an OCaml code generator.
More precisely, I have a development with both Coq and OCaml code (in the style of CompCert, for instance). I’ve been able to set up a build system using dune by splitting the development into three parts: a pure Coq part and a pure OCaml part, both using dune; and a hackish glue that runs coqc extraction.v to populate the source tree.
I wished there were a better way.