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

                                                                                           COQ(1)