Scroll to navigation

COQ(1) General Commands Manual COQ(1)


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

print Coq's standard library location and exit

print Coq version and exit

skip loading of rcfile (resource file) if any

-init-file filename
set the rcfile to filename

batch mode (exits just after arguments parsing)

tells Coq it is executed under Emacs

-dump-glob filename
dump globalizations in file f (to be used by coqdoc(1) )

set sort Set impredicative

don't load opaque proofs in memory


coqc(1), coq-tex(1), coqdep(1).
The Coq Reference Manual. The Coq web site:
October 11, 2006