通過在Coq中使用「遞歸提取」提取到OCaml文件

Question

我想將Coq中的函數foo提取爲OCaml文件。因爲我的真實功能必須使用Recursive Extraction，所以當我運行一個程序時，它會在cmd上輸出提取的OCaml代碼。但我想它輸出到文件，例如：foo.ml

Recursive Extraction foo. 

當我想：

Recursive Extraction "foo.ml" foo. 

或Recursive Extraction foo "foo.ml"

我得到了一個錯誤：Syntax error: "." expected after [vernac:command] (in [vernac_aux]).

我問題是：我能否使用Recursive Extraction語法將函數foo提取到文件？感謝您的幫助。

Answer 1

根據手冊（http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual027.html），Extraction "foo.ml" foo將提取foo和遞歸所有的依賴到foo.ml，即你不要在這種情況下需要Recursive，它僅用於在標準輸出上提取。