NAME¶

coqnative - native Coq 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 to -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