.TH COQTOP 1
.
.SH NAME
coqtop \- toplevel Coq system
.
.
.SH SYNOPSIS
.B coqtop
[
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
.BR \-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
.BR \-require .
.
.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
.I filename
(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.
.
.SH SEE ALSO
.
.BR coqc (1),
.BR coq-tex (1),
.BR coqdep (1)
.PP
.I
The Rocq Prover Reference Manual.
.PP
The Rocq Prover website:
https://rocq-prover.org
