Man pages sections > man1 > coqtop

coqtop - The Coq Proof Assistant toplevel system

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-object filename
load ML object file filenname
 
-load-ml-source filename
load ML file filename
 
-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.)
 
-load-vernac-object path
load Coq library path (Require path.)
 
-require path
load Coq library path and import it (Require Import path.)
 
-compile filename.v
compile Coq file filename.v (implies -batch )
 
-compile-verbose filename.v
verbosely compile Coq file filename.v (implies -batch )
 
-where
print Coq's standard library location and exit
 
-v
print Coq version and exit
 
-q
skip loading of rcfile
 
-init-file filename
set the rcfile to filename
 
-batch
batch mode (exits just after arguments parsing)
 
-boot
boot mode (implies -q and -batch )
 
-emacs
tells Coq it is executed under Emacs
 
-dump-glob filename
dump globalizations in file f (to be used by coqdoc(1) )
 
-with-geoproof (yes|no)
to (de)activate special functions for Geoproof within Coqide (default is yes )
 
-impredicative-set
set sort Set impredicative
 
-dont-load-proofs
don't load opaque proofs in memory
 
-xml
export XML files either to the hierarchy rooted in the directory $COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset)
 

SEE ALSO

coqc(1), coq-tex(1), coqdep(1).
 
The Coq Reference Manual. The Coq web site: http://coq.inria.fr
October 11, 2006 Debian Sid