Control de la exportación de constructores en código extraído de Coq

Question

Estoy buscando escribir código en Coq y extraer este código para usar en un gran proyecto de Haskell. Quiero construir un único módulo en Coq, probar propiedades y luego usar el sistema de módulos de Haskell para evitar la violación de estas propiedades (a través de constructores inteligentes).

No encuentro ninguna indicación de que sea posible extraer el código Coq en un módulo Haskell con una lista de exportación explícita. Parece que debo modificar manualmente el código Coq extraído, lo cual no es gran cosa, pero quiero saber si tengo este derecho. ¿Alguien tiene una propuesta alternativa?

Answer 1

Acabo de ver la última fuente de coq (r14456). No parece haber ningún código para generar una lista de exportación.

Parece que tendrá que hacer esto usted mismo.