.TH COQC 1
.
.SH NAME
coqc \- Coq compiler
.
.
.SH SYNOPSIS
.B coqc
[
general Coq options
]
.I file
.
.
.SH DESCRIPTION
.
.B coqc
is the batch compiler for the Coq Proof Assistant.
The options are basically the same as
.BR coqtop (1).
.I file.v
is the vernacular file to compile.
.I 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
.IR file.vo \&.
.PP
For interactive use of Coq, see
.BR coqtop (1).
.
.
.SH OPTIONS
.
.\" TODO: Coqc is not a script.  Correct this claim.
.B coqc
is a script that simply runs
.B coqtop
with option
.BR \-compile .
It accepts the same options as
.BR coqtop .
.
.TP
.BI \-image \ bin
Use
.I bin
as underlying
.B coqtop
instead of the default one.
.
.TP
.B \-verbose
Print the compiled file on the standard output.
.
.SH SEE ALSO
.
.BR coqtop (1),
.BR coq_makefile (1),
.BR coqdep (1)
.PP
.I
The Rocq Prover Reference Manual.
.PP
The Rocq Prover website: https://rocq-prover.org