coqnative - native Coq compiler
Contents
Description
coqnative compiles vo files to binary files used by the native compute mechanism of the Coq Proof
Assistant. See the ReferenceManual 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.
Name
coqnative - native Coq compiler
Options
-Qdircoqdir
Map physical dir to logical coqdir.-Rdircoqdir
Synonymous to -Q.
-Idir Ignored, for compatibility.
-noinit
Ignored, for compatibility.
-boot Boot mode.
-coqlibdir
Override the default location of the standard library.
-nIdir
Add dir to the set of paths for the native files of the dependencies.
-native-output-dirdir
Output the generated files to dir.-h, --help
Print list of options.
See Also
coqtop(1), coqc(1), coq_makefile(1), coqdep(1) TheCoqReferenceManual. The Coq web site: http://coq.inria.frCOQNATIVE(1)
Synopsis
coqnative [ options ] filename
