Controlling exportation of constructors in code extracted from Coq

Question

I'm looking at writing code in Coq and extracting this code for use in a large Haskell project. I want to build a single module in Coq, prove properties, then use Haskell's module system to prevent violation of these properties (via smart constructors).

I can't find any indication that it's possible to extract Coq code into a Haskell module with an explicit export list. It seems I must hand-modify the extracted Coq code, which isn't a big deal but I want to know if I have this right. Does anyone have an alternate proposal?

Answer 1

I just looked at the latest coq source (r14456). There doesn't seem to be any code to generate an export list.

Seems you'll have to do this yourself.