## 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