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 Coq Reference Manual.

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

                                                                                        COQTOP(1)