COQ

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

−inputstate filename, −is filename

read state from file filename.coq

−nois

start with an empty intial state

−outputstatefilename

write state in file filename.coq

−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 filename

load Coq object file filename.vo

−require filename

load Coq object file filename.vo and import it (Require Import filename.)

−compile filename

compile Coq file filename.v (implies −batch )

−compile−verbose filename

verbosely compile Coq file filename.v (implies −batch )

−opt

run the native−code version of Coq

−byte

run the bytecode version of Coq

−where

print Coq’s standard library location and exit

−v

print Coq version and exit

−q

skip loading of rcfile

−init−file filename

set the rcfile to filename

−user uid

use the rcfile of user uid

−batch

batch mode (exits just after arguments parsing)

−boot

boot mode (implies −q and −batch )

−emacs

tells Coq it is executed under Emacs

−dump−glob filename

dump globalizations in file f (to be used by coqdoc(1) )

−with−geoproof (yes|no)

to (de)activate special functions for Geoproof within Coqide (default is yes )

−impredicative−set

set sort Set impredicative

−dont−load−proofs

don’t load opaque proofs in memory

−xml

export XML files either to the hierarchy rooted in the directory $COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset)

−quality

improve the legibility of the proof terms produced by some tactics

coqc(1), coq-tex(1), coqdep(1).
The Coq Reference Manual. The Coq web site: http://coq.inria.fr