COQ(1) | General Commands Manual | COQ(1) |
coqnative - The Coq native compiler
coqnative [ options ] filename
coqnative compiles vo files to binary files used by the native compute mechanism of the Coq Proof Assistant. See the Reference Manual for more information. It returns with exit code 0 if all the requested tasks succeeded. A non-zero return code means that something went wrong.
filename is a Coq object file (a .vo) to compile to a native binary.
coqtop(1), coqc(1), coq_makefile(1),
coqdep(1).
The Coq Reference Manual. The Coq web site:
http://coq.inria.fr