ssrcoq1

The coq proof assistant toplevel system

Usage

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

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

`-init-file filename`	set the rcfile to filename
`-user uid`	use the rcfile of user uid

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

-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

2 releases since Debian 6.0 (Squeeze); the text changed 1 time.