Provided by: coq_8.4pl3dfsg-1_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-inputstatefilename,-isfilenameread state from filefilename.coq-noisstart with an empty initial state-outputstatefilenamewrite state in filefilename.coq-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-objectfilenameload Coq object filefilename.vo-requirefilenameload Coq object filefilename.voand import it (Require Import filename.)-compilefilenamecompile Coq filefilename.v(implies-batch)-compile-verbosefilenameverbosely compile Coq filefilename.v(implies-batch)-optrun the native-code version of Coq-byterun the bytecode version of Coq-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)-qualityimprove the legibility of the proof terms produced by some tactics

**SEE** **ALSO**

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