Stream: Coq users

Topic: Extracting with other OCaml files

view this post on Zulip Josh Cohen (Mar 12 2024 at 20:47):

I am using dune to build a project that will have a mix of .ml files produced by extraction as well as handwritten .ml files. What is the best way to combine these so that dune can see all of the relevant files and compile without extra qualified names everywhere?

I have a very small test available at, but the only way I can get the resulting .ml files to compile is by using a qualified name (in the example, I can extract bigint to A.BigInt.t but not just BigInt.t). Is there a way to structure the directories or the dune files to allow unqualified names? Thanks

Last updated: Jun 23 2024 at 05:02 UTC