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
