coqtop(1)
| COQTOP(1) | General Commands Manual | COQTOP(1) |
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.
SEE ALSO
coqc(1), coq-tex(1), coqdep(1)
The Rocq Prover Reference Manual.
The Rocq Prover website: https://rocq-prover.org