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 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	depen-
	      dencies.

       -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.0.quarterly>

home | help