DOKK / manpages / debian 10 / coq / coqc.1.en
COQ(1) General Commands Manual COQ(1)

coqc - The Coq Proof Assistant compiler

coqc [ general  Coq  options ] file

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

coqc is a script that simply runs coqtop with option -compile it accepts the same options as coqtop.

use bin as underlying coqtop instead of the default one.

print the compiled file on the standard output.

coqtop(1), coq_makefile(1), coqdep(1).
The Coq Reference Manual. The Coq web site: http://coq.inria.fr

April 25, 2001