CoqをHaskellに抽出する際にモジュール名を設定する方法

Question

Coqファイル内でExtraction Language Haskell.を使用してCoqをHaskellに抽出/コンパイルするときにcoqtop -compile mymodule.v > MyModule.hsを実行すると、module Main whereで始まるHaskellモジュールが得られます。

結果のHaskellモジュール名を設定するオプションはありますか？

I現在、パイプ

は次のようにsedをする -

coqtop -compile mymodule.v | sed s/Main/MyModule/ > MyModule.hs 

が、私はクリーンな解決策を探しています。

Answer 1

Extraction "file"またはExtraction Library（またはその変形）を使用できます。

Definition foo := 6*7. 

Extraction Language Haskell. 
Extraction "MyModule" foo. 

以上がmodule MyModule where始まるMyModule.hsファイルを生成します。