Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Geometry.java   Sprache: Unknown

Untersuchungsergebnis.1 Download desFortran {Fortran[91] Abap[150] [0]}zum Wurzelverzeichnis wechseln

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

[ zur Elbe Produktseite wechseln0.89Quellennavigators  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik