NAME

       coqc - The Coq Proof Assistant 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`-`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

                                          April 25, 2001                                   COQ(1)