Provided by: coq_8.6-5build1_amd64

**NAME**

coqtop - The Coq Proof Assistant toplevel system

**SYNOPSIS**

coqtop[options]

**DESCRIPTION**

coqtopis 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, seecoqc(1).

**OPTIONS**

-h,--helpHelp. Will give you the complete list of options accepted by coqtop.-Idir,--includediradd directorydirin the include path-Rdircoqdirrecursively map physicaldirto logicalcoqdir-topcoqdirset the toplevel name to becoqdirinstead of Top-noisstart with an empty initial state-load-ml-objectfilenameload ML object filefilenname-load-ml-sourcefilenameload ML filefilename-load-vernac-sourcefilename,-lfilenameload Coq filefilename.v(Load filename.)-load-vernac-source-verbosefilename,-lvfilenameload verbosely Coq filefilename.v(Load Verbose filename.)-load-vernac-objectpathload Coq librarypath(Require path.)-requirepathload Coq librarypathand import it (Require Import path.)-compilefilename.vcompile Coq filefilename.v(implies-batch)-compile-verbosefilename.vverbosely compile Coq filefilename.v(implies-batch)-whereprint Coq's standard library location and exit-vprint Coq version and exit-qskip loading of rcfile-init-filefilenameset the rcfile tofilename-batchbatch mode (exits just after arguments parsing)-bootboot mode (implies-qand-batch)-emacstells Coq it is executed under Emacs-dump-globfilenamedump globalizations in file f (to be used bycoqdoc(1))-with-geoproof(yes|no)to (de)activate special functions for Geoproof within Coqide (default isyes)-impredicative-setset sort Set impredicative-dont-load-proofsdon't load opaque proofs in memory-xmlexport XML files either to the hierarchy rooted in the directory $COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset)

**SEE** **ALSO**

coqc(1),coq-tex(1),coqdep(1).TheCoqReferenceManual.TheCoqwebsite:http://coq.inria.frOctober 11, 2006 COQ(1)