NAME¶

coqtop - The Coq Proof Assistant toplevel system

SYNOPSIS¶

coqtop [ options ]

DESCRIPTION¶

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).

OPTIONS¶

-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 initial 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

 

SEE ALSO¶

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