The coq proof assistant toplevel system
coqtop [ options ]
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).
-h, --help
Help. Will give you the complete list of options accepted by coqtop.
-Idir,--includedir
add directory dir in the include path
-Rdircoqdir
recursively map physical dir to logical coqdir
-topcoqdir
set the toplevel name to be coqdir instead of Top
-inputstatefilename,-isfilename
read state from file filename.coq
-nois
start with an empty initial state
-outputstatefilename
write state in file filename.coq
-load-ml-objectfilename
load ML object file filenname
-load-ml-sourcefilename
load ML file filename
-load-vernac-sourcefilename,-lfilename
load Coq file filename.v (Load filename.)
-load-vernac-source-verbosefilename,-lvfilename
load verbosely Coq file filename.v (Load Verbose filename.)
-load-vernac-objectfilename
load Coq object file filename.vo
-requirefilename
load Coq object file filename.vo and import it (Require Import filename.)
-compilefilename
compile Coq file filename.v (implies -batch )
-compile-verbosefilename
verbosely compile Coq file filename.v (implies -batch )
-opt
run the native-code version of Coq
-byte
run the bytecode version of Coq
-where
print Coq's standard library location and exit
-v
print Coq version and exit
-q
skip loading of rcfile
-init-filefilename
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-globfilename
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)
-quality
improve the legibility of the proof terms produced by some tactics
coqc(1), coq-tex(1), coqdep(1).
The Coq Reference Manual. The Coq web site: http://coq.inria.fr