.TH COQ 1

.SH NAME
coqtop \- The Coq Proof Assistant toplevel system


.SH SYNOPSIS
.B coqtop
[
.B options
]

.SH DESCRIPTION

.B coqtop
is the toplevel system of Coq, for interactive use.
It reads phrases on the standard input, and prints results on the
standard output.

For batch-oriented use of Coq, see
.BR coqc(1).


.SH OPTIONS

.TP
.B \-h, \-\-help
Help. Will give you the complete list of options accepted by coqtop.

.TP
.BI \-I \ dir, \ \-\-include \ dir
add directory
.I dir
in the include path

.TP
.BI \-R \ dir\ coqdir
recursively map physical
.I dir
to logical
.I coqdir

.TP
.BI \-top \ coqdir
set the toplevel name to be
.I coqdir
instead of Top

.TP
.B \-nois
start with an empty initial state

.TP
.BI \-load\-ml\-source \ filename
load ML file
.I filename

.TP
.BI \-load\-ml\-object \ filename
load ML object file
.I filenname

.TP
.BI \-load\-vernac\-source \ filename, \ \-l \ filename
load Coq file
.I filename.v
(Load filename.)

.TP
.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename
load verbosely Coq file
.I filename.v
(Load Verbose filename.)

.TP
.BI \-require \ lib
load Coq library
.I lib
(Require lib.)

.TP
.BI \-require-import \ lib, \ \-ri \ lib
load Coq library
.I lib
and import it (Require Import lib.)

.TP
.BI \-require-export \ lib, \ \-re \ lib
load Coq library
.I lib
and transitively import it (Require Export lib.)

.TP
.BI \-require-from \ root\ lib, \ \-rfrom \ root\ lib
load Coq library
.I lib
(From root Require lib.)

.TP
.BI \-require-import-from \ root\ lib, \ \-rifrom \ root\ lib
load Coq library
.I lib
and import it (From root Require Import lib.)

.TP
.BI \-require-export-from \ root\ lib, \ \-refrom \ root\ lib
load Coq library
.I lib
and transitively import it (From root Require Export lib.)

.TP
.BI \-load\-vernac\-object \ lib
obsolete synonym of
.BI \-require \ lib

.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 (resource file) if any

.TP
.BI \-init\-file \ filename
set the rcfile to
.I filename

.TP
.B \-batch
batch mode (exits just after arguments parsing)

.TP
.B \-emacs
tells Coq it is executed under Emacs

.TP
.BI \-dump\-glob \ filename
dump globalizations in file f (to be used by
.B coqdoc(1)
)

.TP
.B \-impredicative\-set
set sort Set impredicative

.TP
.B \-dont\-load\-proofs
don't load opaque proofs in memory

.SH SEE ALSO

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