| COQ(1) | General Commands Manual | COQ(1) |
NAME
coqnative - The Coq native compiler
SYNOPSIS
coqnative [ options ] filename
DESCRIPTION
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.
OPTIONS
- -Q dir coqdir
- map physical dir to logical coqdir
- -R dir coqdir
- synonymous for -Q
- -I dir
- ignored, for compatibility
- -noinit
- ignored, for compatibility
- -boot
- boot mode
- -coqlib dir
- override the default location of the standard library
- -nI dir
- add dir to the set of paths for the native files of the dependencies
- -native-output-dir dir
- output the generated files to dir
- -h, --help
- print list of options
SEE ALSO
coqtop(1), coqc(1), coq_makefile(1),
coqdep(1).
The Coq Reference Manual. The Coq web site:
http://coq.inria.fr