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.

map physical dir to logical coqdir
synonymous for -Q
ignored, for compatibility
ignored, for compatibility
boot mode
override the default location of the standard library
add dir to the set of paths for the native files of the dependencies
output the generated files to dir
print list of options

coqtop(1), coqc(1), coq_makefile(1), coqdep(1).
The Coq Reference Manual. The Coq web site: