Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help 
COQNATIVE(1)		     General Commands Manual		    COQNATIVE(1)

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 suc-
     ceeded.  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  dependen-
	    cies.

     -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

								    COQNATIVE(1)

Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=coqnative&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>

home | help