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

FreeBSD Manual Pages

  
 
  

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

NAME
       coqc - Coq compiler

SYNOPSIS
       coqc [ general Coq options ] file

DESCRIPTION
       coqc  is	 the  batch compiler for the Coq Proof Assistant.  The options
       are basically the same as coqtop(1).  file.v is the vernacular file  to
       compile.	  file must be formed only with	the characters `a' to `Z', `0'
       to `9' or `_' and must begin with a letter.  The	compiler  produces  an
       object file file.vo.

       For interactive use of Coq, see coqtop(1).

OPTIONS
       coqc  is	a script that simply runs coqtop with option -compile.	It ac-
       cepts the same options as coqtop.

       -image bin
	      Use bin as underlying coqtop instead of the default one.

       -verbose
	      Print the	compiled file on the standard output.

SEE ALSO
       coqtop(1), coq_makefile(1), coqdep(1)

       The Coq Reference Manual.

       The Coq web site: http://coq.inria.fr

								       COQC(1)

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

home | help