coqtop man page

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

-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 (resource file) if any

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


set sort Set impredicative


don't load opaque proofs in memory

See Also

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

Referenced By

coqc(1), coqchk(1), coqide(1), coq_makefile(1), coqtop.byte(1), coqtop.opt(1).

October 11, 2006