NAME¶

coqtop - The Coq Proof Assistant toplevel system

SYNOPSIS¶

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
-nois: 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.)
-where: print Coq's standard library location and exit
-v: print Coq version and exit
-q: skip loading of rcfile (resource file) if any
-init-file filename: set the rcfile to filename
-batch: batch mode (exits just after arguments parsing)
-emacs: tells Coq it is executed under Emacs
-dump-glob filename: dump globalizations in file f (to be used by coqdoc(1) )
-impredicative-set: set sort Set impredicative
-dont-load-proofs: don't load opaque proofs in memory