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  accepts  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)