Coq2SML Coq2SMLはExtractionをStandard MLに対応させる非公式のCoq改造です。 この改造に関する問い合わせは公式ではなくこちらにお願いします。 インストール方法 通常のCoqと同様の方法でインストールできます。 coq-8.4pl4/INSTALLを参照して下さい。 使用方法 Extraction Language Sml. と書く事で、以降のExtractionでStandard MLのソースコードが出力されます。