summaryrefslogtreecommitdiff
path: root/man/coqide.1
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
commit113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (patch)
treec260a140410c796f113584a2f7e6b9b7f6e00aa5 /man/coqide.1
parent870075f34dd9fa5792bfbf413afd3b96f17e76a0 (diff)
Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg
Diffstat (limited to 'man/coqide.1')
-rw-r--r--man/coqide.1166
1 files changed, 166 insertions, 0 deletions
diff --git a/man/coqide.1 b/man/coqide.1
new file mode 100644
index 00000000..20379ef4
--- /dev/null
+++ b/man/coqide.1
@@ -0,0 +1,166 @@
+.TH COQIDE 1 "July 16, 2004"
+
+.SH NAME
+coqide \- The Coq Proof Assistant graphical interface
+
+
+.SH SYNOPSIS
+.B coqide
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B coqtop
+is a gtk graphical interface for the Coq proof assistant.
+
+For command-line-oriented use of Coq, see
+.BR coqide (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
+.BI \-is\ f ,\ \-inputstate\ f
+Read state from
+.IR f .coq.
+.TP
+.B \-nois
+Start with an empty state.
+.TP
+.BI \-outputstate\ f
+Write state in file
+.IR f .coq.
+.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\ f
+Load Coq object file
+.IR f .vo.
+.TP
+.BI \-require\ f
+Load Coq object file
+.IR f .vo
+and import it (Require
+.IR f .).
+.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 \-opt
+Run the native-code version of Coq or Coq_SearchIsos.
+.TP
+.B \-byte
+Run the bytecode version of Coq or Coq_SearchIsos.
+.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
+.BI \-user\ u
+Use the rcfile of user
+.IR u .
+.TP
+.B \-batch
+Batch mode (exits just after arguments parsing).
+.TP
+.B \-boot
+Boot mode (implies
+.B \-q
+and
+.BR \-batch ).
+.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.
+.TP
+.B \-xml
+Export XML files either to the hierarchy rooted in
+the directory
+.B COQ_XML_LIBRARY_ROOT
+(if set) or to stdout (if unset).
+
+
+.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).