COQTOP(1) General Commands Manual COQTOP(1)

coqtop - toplevel Coq system

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

Help. Will give you the complete list of options accepted by coqtop.
Add directory dir in the include path.
Recursively map physical dir to logical coqdir.
Set the toplevel name to be coqdir instead of Top.
Start with an empty initial state.
Load ML file filename.
Load ML object file filenname.
Load Coq file filename.v. (Load filename.)
Load verbosely Coq file filename.v. (Load Verbose filename.)
Load Coq library lib. (Require lib.)
Load Coq library lib and import it. (Require Import lib.)
Load Coq library lib and transitively import it. (Require Export lib.)
Load Coq library lib. (From root Require lib.)
Load Coq library lib and import it. (From root Require Import lib.)
Load Coq library lib and transitively import it. (From root Require Export lib.)
Obsolete synonym of -require.
Print Coq's standard library location and exit.
Print Coq version and exit.
Skip loading of rcfile (resource file) if any.
Set the rcfile to filename.
Batch mode (exits just after arguments parsing).
Tells Coq it is executed under Emacs.
Dump globalizations in file filename (to be used by coqdoc(1)).
Set sort Set impredicative.
Don't load opaque proofs in memory.

coqc(1), coq-tex(1), coqdep(1)

The Coq Reference Manual.

The Coq web site: http://coq.inria.fr