Provided by: coq_8.15.2+dfsg-2_amd64
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 -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
coqc(1), coq-tex(1), coqdep(1). The Coq Reference Manual. The Coq web site: http://coq.inria.fr COQ(1)