coq - Coqの「再帰的抽出」を使用してOCamlファイルに抽出します

Question

foo関数をファイルCoqに抽出したい。OCaml私の実際の関数は を使用する必要があるためRecursive Extraction、プログラムを実行すると、抽出された OCaml コードが に出力されますcmd。しかし、たとえば次のようにファイルに出力したいと思います。foo.ml

Recursive Extraction foo.

私が試したとき：

Recursive Extraction "foo.ml" foo.

またRecursive Extraction foo "foo.ml"

エラーが発生しました：Syntax error: "." expected after [vernac:command] (in [vernac_aux]).

私の質問は次のとおりです。構文fooを使用して関数をファイルに抽出できますか? Recursive Extractionご協力ありがとうございました。

Answer 1

マニュアル ( http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual027.html ) によると、すべての依存関係を再帰的Extraction "foo.ml" fooに抽出し、その場合は必要ありません。stdout での抽出にのみ使用されます。foofoo.mlRecursive