From 26a8b0de6e7daef17f113c30e02a9aae43edddfc Mon Sep 17 00:00:00 2001 From: glondu Date: Tue, 12 Aug 2008 13:41:58 +0000 Subject: Add coqide manpage (taken from Debian) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11324 85f007b7-540e-0410-9357-904b9bb8a0f7 --- man/coqide.1 | 166 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 166 insertions(+) create mode 100644 man/coqide.1 (limited to 'man') diff --git a/man/coqide.1 b/man/coqide.1 new file mode 100644 index 000000000..20379ef4d --- /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 , +for the Debian project (but may be used by others). -- cgit v1.2.3