rahmenlose Ansicht.1 DruckansichtFortran {Fortran[91] Abap[150] [0]}Entwicklung
.TH COQ 1 "October 11, 2006"
.SH NAME
coqtop \- The Coq Proof Assistant toplevel system
.SH SYNOPSIS
.B coqtop
[
.B options
]
.SH DESCRIPTION
.B 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
.BR coqc(1).
.SH OPTIONS
.TP
.B \-h, \-\-help
Help. Will give you the complete list of options accepted by coqtop.
.TP
.BI \-I \ dir, \ \-\-include \ dir
add directory
.I dir
in the include path
.TP
.BI \-R \ dir\ coqdir
recursively map physical
.I dir
to logical
.I coqdir
.TP
.BI \-top \ coqdir
set the toplevel name to be
.I coqdir
instead of Top
.TP
.B \-nois
start with an empty initial state
.TP
.BI \-load\-ml\-object \ filename
load ML object file
.I filenname
.TP
.BI \-load\-ml\-source \ filename
load ML file
.I filename
.TP
.BI \-load\-vernac\-source \ filename, \ \-l \ filename
load Coq file
.I filename.v
(Load filename.)
.TP
.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename
load verbosely Coq file
.I filename.v
(Load Verbose filename.)
.TP
.BI \-load\-vernac\-object \ path
load Coq library
.I path
(Require path.)
.TP
.BI \-require \ path
load Coq library
.I path
and import it (Require Import path.)
.TP
.B \-where
print Coq's standard library location and exit
.TP
.B \-v
print Coq version and exit
.TP
.B \-q
skip loading of rcfile (resource file) if any
.TP
.BI \-init\-file \ filename
set the rcfile to
.I filename
.TP
.B \-batch
batch mode (exits just after arguments parsing)
.TP
.B \-emacs
tells Coq it is executed under Emacs
.TP
.BI \-dump\-glob \ filename
dump globalizations in file f (to be used by
.B coqdoc(1)
)
.TP
.B \-impredicative\-set
set sort Set impredicative
.TP
.B \-dont\-load\-proofs
don't load opaque proofs in memory
.SH SEE ALSO
.BR coqc (1),
.BR coq-tex (1),
.BR coqdep (1).
.br
.I
The Coq Reference Manual.
.I
The Coq web site: http://coq.inria.fr
[ Verzeichnis aufwärts0.154unsichere Verbindung
]
