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

Help. Will give you the complete list of options accepted by coqtop.
add directory dir in the include path
recursively map physical dir to logical coqdir
set the toplevel name to be coqdir instead of Top
start with an empty initial state
load ML object file filenname
load ML file filename
load Coq file filename.v (Load filename.)
load verbosely Coq file filename.v (Load Verbose filename.)
load Coq library 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
set the rcfile to filename
batch mode (exits just after arguments parsing)
tells Coq it is executed under Emacs
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: