I want to extract a function foo in Coq to an OCaml file. Because my real function have to use the Recursive Extraction, when I run a program it output the extracted OCaml code on the cmd. But I would like to output it to a file, for example: foo.ml
Recursive Extraction foo.
When I tried:
Recursive Extraction "foo.ml" foo.
or Recursive Extraction foo "foo.ml"
I got an error: Syntax error: "." expected after [vernac:command] (in [vernac_aux]).
My question is: Am I able to extract the function foo to a file by using the Recursive Extraction syntax? Thank you for your help.
According to the manual (http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual027.html), Extraction "foo.ml" foo will extract foo and recursively all its dependencies into foo.ml, i.e. you don't need Recursive in that case, it is only used for extraction on stdout.