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

-nois

start with an empty initial state

-load-ml-source filename

load ML file filename

-load-ml-object filename

load ML object file filenname

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

-require lib

load Coq library lib (Require lib.)

-require-import lib, -ri lib

load Coq library lib and import it (Require Import lib.)

-require-export lib, -re lib

load Coq library lib and transitively import it (Require Export lib.)

-require-from root lib, -rfrom root lib

load Coq library lib (From root Require lib.)

-require-import-from root lib, -rifrom root lib

load Coq library lib and import it (From root Require Import lib.)

-require-export-from root lib, -refrom root lib

load Coq library lib and transitively import it (From root Require Export lib.)

-load-vernac-object lib

obsolete synonym of -require lib

-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

SEE ALSO¶

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