coqtop (1)
NAME
coqtop - The Coq Proof Assistant toplevel systemSYNOPSIS
coqtop [ options ]DESCRIPTION
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 coqc(1).
OPTIONS
- -h, --help
-
Help. Will give you the complete list of options accepted by coqtop.
- -I dir, --include dir
-
add directory
dir
in the include path
- -R dir coqdir
-
recursively map physical
dir
to logical
coqdir
- -top coqdir
-
set the toplevel name to be
coqdir
instead of Top
- -nois
-
start with an empty initial state
- -load-ml-object filename
-
load ML object file
filenname
- -load-ml-source filename
-
load ML file
filename
- -load-vernac-source filename, -l filename
-
load Coq file
filename.v
(Load filename.)
- -load-vernac-source-verbose filename, -lv filename
-
load verbosely Coq file
filename.v
(Load Verbose filename.)
- -load-vernac-object path
-
load Coq library
path
(Require path.)
- -require path
-
load Coq library
path
and import it (Require Import path.)
- -compile filename.v
-
compile Coq file
filename.v
(implies
-batch
)
- -compile-verbose filename.v
-
verbosely compile Coq file
filename.v
(implies
-batch
)
- -where
-
print Coq's standard library location and exit
- -v
-
print Coq version and exit
- -q
-
skip loading of rcfile
- -init-file filename
-
set the rcfile to
filename
- -batch
-
batch mode (exits just after arguments parsing)
- -boot
-
boot mode (implies
-q
and
-batch
)
- -emacs
-
tells Coq it is executed under Emacs
- -dump-glob filename
-
dump globalizations in file f (to be used by
coqdoc(1)
)
- -with-geoproof (yes|no)
-
to (de)activate special functions for Geoproof within Coqide (default is
yes
)
- -impredicative-set
-
set sort Set impredicative
- -dont-load-proofs
-
don't load opaque proofs in memory
- -xml
-
export XML files either to the hierarchy rooted in
the directory $COQ_XML_LIBRARY_ROOT (if set) or to
stdout (if unset)
SEE ALSO
coqc(1), coq-tex(1), coqdep(1).
The Coq Reference Manual. The Coq web site: coq.inria.fr