logo
Free, unlimited AI code reviews that run on commit
git-lrc git-lrc GitHub Install Now We'd appreciate a star git-lrc - Free, unlimited AI code reviews that run on commit | Product Hunt git-lrc - Free, unlimited AI code reviews that run on commit | Product Hunt

coqnative - native Coq compiler

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

See Also