.TH COQ 1 "April 25, 2001"

.SH NAME
coqc \- The Coq Proof Assistant compiler


.SH SYNOPSIS
.B coqc
[
.B 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 coqtop(1).
.IR file.v \&
is the vernacular file to compile.
.IR 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
.IR file.vo \&.

For interactive use of Coq, see 
.BR coqtop(1).


.SH OPTIONS

.TP
.BI \-h
Show the whole list of options of coqc and coqtop.
.TP
.B \-verbose
Compile verbosely.
.TP
.BI \-image\  f
Specify an alternative executable for Coq.
.TP
.B \-t
Keep temporary files.
.TP
.BI \-I\  dir ,\ \-include\  dir
Add directory dir in the include path.
.TP
.BI \-R\  dir\ coqdir
Recursively map physical dir to logical coqdir.
.TP
.B \-src
Add source directories in the include path.
.TP
.BI \-is\  f ,\ \-inputstate\  f
Read state from file
.IR f .coq.
.TP
.B \-nois
Start with an empty state.
.TP
.BI \-outputstate\  f
Write state in file
.IR f .coq.
.TP
.BR \-load\-ml\-object\  f
Load ML object file
.IR f .
.TP
.BI \-load\-ml\-source\  f
Load ML file
.IR f .
.TP
.BI \-l\  f ,\ \-load\-vernac\-source\  f
Load Coq file
.IR f .v
(Load
.IR f .).
.TP
.BI \-lv\  f ,\ \-load\-vernac\-source\-verbose\  f
Load Coq file
.IR f .v
(Load Verbose
.IR f .).
.TP
.BI \-load\-vernac\-object\  f
Load Coq object file
.IR f .vo.
.TP
.BI \-require\  f
Load Coq object file
.IR f .vo
and import it (Require
.IR f .).
.TP
.BI \-compile\  f
Compile Coq file
.IR f .v
(implies
.BR \-batch ).
.TP
.BI \-compile\-verbose\  f
Verbosely compile Coq file
.IR f .v
(implies
.BR \-batch ).
.TP
.B \-opt
Run the native-code version of Coq or Coq_SearchIsos.
.TP
.B \-byte
Run the bytecode version of Coq or Coq_SearchIsos.
.TP
.B \-where
Print Coq's standard library location and exit.
.TP
.B \-v
Print Coq version and exit.
.TP
.B \-q
Skip loading of rcfile.
.TP
.BI \-init\-file\  f
Set the rcfile to
.IR f .
.TP
.BI \-user\  u
Use the rcfile of user
.IR u .
.TP
.B \-batch
Batch mode (exits just after arguments parsing).
.TP
.B \-boot
Boot mode (implies
.B \-q
and
.BR \-batch ).
.TP
.B \-emacs
Tells Coq it is executed under Emacs.
.TP
.BI \-dump\-glob\  f
Dump globalizations in file
.I f
(to be used by
.BR coqdoc (1)).
.TP
.B \-impredicative\-set
Set sort Set impredicative.
.TP
.B \-dont\-load\-proofs
Don't load opaque proofs in memory.
.TP
.B \-xml
Export XML files either to the hierarchy rooted in
the directory 
.B COQ_XML_LIBRARY_ROOT
(if set) or to stdout (if unset).

.SH SEE ALSO

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