coqtop - Man Page

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

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), coqnative(1), coqtop.byte(1), coqtop.opt(1).