coqtop - toplevel Coq system

NAME SYNOPSIS DESCRIPTION OPTIONS SEE ALSO

NAME

coqtop − toplevel Coq 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.

	−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 filename (to be used by coqdoc(1)).

−impredicative−set

Set sort Set impredicative.

−dont−load−proofs

Don’t load opaque proofs in memory.