COQ(1) | General Commands Manual | COQ(1) |
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