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

                                                                                           COQ(1)