coqtop(1) 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.

-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

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 )

print Coq's standard library location and exit

print Coq version and exit

skip loading of rcfile

-init-file filename
set the rcfile to filename

batch mode (exits just after arguments parsing)

boot mode (implies -q and -batch )

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 )

set sort Set impredicative

don't load opaque proofs in memory

export XML files either to the hierarchy rooted in the directory $COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset)