.TH COQIDE 1

.SH NAME
coqide \- The Coq Proof Assistant graphical interface


.SH SYNOPSIS
.B coqide
[
.B options
]

.SH DESCRIPTION

.B coqide
is a gtk graphical interface for the Coq proof assistant.

For command-line-oriented use of Coq, see
.BR coqtop (1)
; for batch-oriented use of Coq, see
.BR coqc (1).


.SH OPTIONS

.TP
.B \-h
Show the complete list of options accepted by
.BR coqide .
.TP
.BI \-I\  dir ,\ \-include\  dir
Add directory dir in the include path.
.TP
.BI \-R\  dir\ coqdir
Recursively map physical
.I dir
to logical
.IR coqdir .
.TP
.B \-src
Add source directories in the include path.
.TP
.B \-nois
Start with an empty state.
.TP
.BI \-load\-ml\-object\  f
Load ML object file
.IR f .
.TP
.BI \-load\-ml\-source\  f
Load ML file
.IR f .
.TP
.BI \-l\  f ,\ \-load\-vernac\-source\  f
Load Coq file
.IR f .v
(Load
.IR f .).
.TP
.BI \-lv\  f ,\ \-load\-vernac\-source\-verbose\  f
Load Coq file
.IR f .v
(Load Verbose
.IR f .).
.TP
.BI \-load\-vernac\-object\  path
Load Coq library
.IR path
(Require
.IR path .).
.TP
.BI \-require-import\  path
Load Coq library
.IR path
and import it (Require Import
.IR path .).
.TP
.BI \-compile\  f
Compile Coq file
.IR f .v
(implies
.BR \-batch ).
.TP
.BI \-compile\-verbose\  f
Verbosely compile Coq file
.IR f .v
(implies
.BR -batch ).
.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.
.TP
.BI \-init\-file\  f
Set the rcfile to
.IR f .
.TP
.B \-emacs
Tells Coq it is executed under Emacs.
.TP
.BI \-dump\-glob\  f
Dump globalizations in file
.I f
(to be used by
.BR 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 coqtop (1),
.BR coq-tex (1),
.BR coqdep (1).
.br
.I
The Coq Reference Manual,
.I
The Coq web site: http://coq.inria.fr,
.I
/usr/share/doc/coqide/FAQ.

.SH AUTHOR
This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>,
for the Debian project (but may be used by others).