From 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 8 Sep 2008 00:15:04 +0200 Subject: Imported Upstream version 8.2~beta4.svn20080907+dfsg --- man/coq-interface.1 | 4 +- man/coq-parser.1 | 30 ++++++++++ man/coq-tex.1 | 22 +++---- man/coqdep.1 | 10 ++-- man/coqdoc.1 | 38 ++++++------ man/coqide.1 | 166 ++++++++++++++++++++++++++++++++++++++++++++++++++++ man/coqmktop.1 | 6 +- man/coqwc.1 | 2 +- man/parser.1 | 30 ---------- 9 files changed, 237 insertions(+), 71 deletions(-) create mode 100644 man/coq-parser.1 create mode 100644 man/coqide.1 delete mode 100644 man/parser.1 (limited to 'man') diff --git a/man/coq-interface.1 b/man/coq-interface.1 index 2ab2bf95..ee013d95 100644 --- a/man/coq-interface.1 +++ b/man/coq-interface.1 @@ -1,7 +1,7 @@ .TH COQ 1 "April 25, 2001" .SH NAME -coq-interface \- +coq\-interface \- Customized Coq toplevel to make user interfaces .SH SYNOPSIS @@ -29,7 +29,7 @@ coq-interface (the same as coqtop). .BR coqc (1), .BR coqdep (1), .BR coqtop (1), -.BR parser (1). +.BR coq\-parser (1). .br .I The Coq Reference Manual. diff --git a/man/coq-parser.1 b/man/coq-parser.1 new file mode 100644 index 00000000..23dc8201 --- /dev/null +++ b/man/coq-parser.1 @@ -0,0 +1,30 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coq\-parser \- Coq parser + + +.SH SYNOPSIS +.B coq\-parser +[ +.B options +] + +.SH DESCRIPTION + +.B parser +is a program reading Coq proof developments and outputing them in the +structured format given in the INRIA technical report RT154. This +program is not for the casual user. + +.SH SEE ALSO + +.BR coq\-interface (1), +.BR coqc (1), +.BR coqtop (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/man/coq-tex.1 b/man/coq-tex.1 index 737de70a..7e0a2f81 100644 --- a/man/coq-tex.1 +++ b/man/coq-tex.1 @@ -15,19 +15,19 @@ coq-tex \- Process Coq phrases embedded in LaTeX files .BI \-image \ coq-image ] [ -.B -w +.B \-w ] [ -.B -v +.B \-v ] [ -.B -sl +.B \-sl ] [ -.B -hrule +.B \-hrule ] [ -.B -small +.B \-small ] .I input-file ... @@ -75,7 +75,7 @@ typewriter font. .TP .BI \-o \ output-file Specify the name of a file where the LaTeX output is to be stored. A -dash `-' causes the LaTeX output to be printed on standard output. +dash `\-' causes the LaTeX output to be printed on standard output. .TP .BI \-n \ line-width Set the line width. The default is 72 characters. The responses of the @@ -90,23 +90,23 @@ this is the command .IR coqtop without specifying any path which is used to evaluate the Coq phrases. .TP -.B -w +.B \-w Cause lines to be folded on a space character whenever possible, avoiding word cuts in the output. By default, folding occurs at the line width, regardless of word cuts. .TP -.B -v +.B \-v Verbose mode. Prints the Coq answers on the standard output. Useful to detect errors in Coq phrases. .TP -.B -sl +.B \-sl Slanted mode. The Coq answers are written in a slanted font. .TP -.B -hrule +.B \-hrule Horizontal lines mode. The Coq parts are written between two horizontal lines. .TP -.B -small +.B \-small Small font mode. The Coq parts are written in a smaller font. diff --git a/man/coqdep.1 b/man/coqdep.1 index 6ae89f8b..e2cbb40e 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -67,7 +67,7 @@ Prints a warning if a Coq command .IR Module \& is incorrect. (For instance, you wrote `Declare ML Module "A".', but the module A contains #open "B"). The correct command is printed -(see option -D). The warning is printed on standard error. +(see option \-D). The warning is printed on standard error. .TP .BI \-i Prints also the dependencies for .vi files (Coq specification modules). @@ -138,7 +138,7 @@ Z.v contains the commands `Require X' and `Declare ML Module "D"'. To get the dependencies of the Coq files: .IP .B -example% coqdep -I . *.v +example% coqdep \-I . *.v .RS .sp .5 .nf @@ -153,7 +153,7 @@ example% coqdep -I . *.v With a warning: .IP .B -example% coqdep -w -I . *.v +example% coqdep \-w \-I . *.v .RS .sp .5 .nf @@ -170,7 +170,7 @@ example% coqdep -w -I . *.v To get only the Caml dependencies: .IP .B -example% coqdep -c -I . *.ml +example% coqdep \-c \-I . *.ml .RS .sp .5 .nf @@ -190,4 +190,4 @@ example% coqdep -c -I . *.ml .SH BUGS Please report any bug to -.B coq-bugs@pauillac.inria.fr +.B coq\-bugs@pauillac.inria.fr diff --git a/man/coqdoc.1 b/man/coqdoc.1 index c443e8b0..45fcafd2 100644 --- a/man/coqdoc.1 +++ b/man/coqdoc.1 @@ -54,7 +54,7 @@ Redirect the output into the file Output files into directory .I dir instead of current directory (option --d does not change the filename specified with option -o, if any). +\-d does not change the filename specified with option \-o, if any). .TP .B \-s, \ \-\-short Do not insert titles for the files. The default behavior is to insert @@ -68,7 +68,7 @@ Suppress the header and trailer of the final document. Thus, you can insert the resulting document into a larger one. .TP .BI \-p \ string, \ \-\-preamble \ string -Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with -html). +Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with \-html). .TP .BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file Considers the file `file' respectively as a .v (or .g) file or a .tex file. @@ -114,7 +114,7 @@ it builds a table of contents into toc.html. .TP .B \-\-glob\-from \ file Make references using Coq globalizations from file file. (Such -globalizations are obtained with Coq option -dump-glob). +globalizations are obtained with Coq option \-dump\-glob). .TP .B \-\-no\-externals @@ -129,22 +129,22 @@ Set base URL for the Coq standard library (default is http://coq.inria.fr/librar Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css. .TP -.BI -R \ dir \ coqdir +.BI \-R \ dir \ coqdir Map physical directory dir to Coq logical directory coqdir (similarly -to Coq option -R). +to Coq option \-R). .B Note: -option -R only has effect on the files following it on the command +option \-R only has effect on the files following it on the command line, so you will probably need to put this option first. .SS Contents options .TP -.B -g, \ --gallina +.B \-g, \ \-\-gallina Do not print proofs. .TP -.B -l, \ --light -Light mode. Suppress proofs (as with -g) and the following commands: +.B \-l, \ \-\-light +Light mode. Suppress proofs (as with \-g) and the following commands: * [Recursive] Tactic Definition * Hint / Hints @@ -153,29 +153,29 @@ Light mode. Suppress proofs (as with -g) and the following commands: * Implicit Argument / Implicits * Section / Variable / Hypothesis / End -The behavior of options -g and -l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above). +The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above). .SS Language options Default behavior is to assume ASCII 7 bits input files. .TP -.B -latin1, \ --latin1 -Select ISO-8859-1 input files. It is equivalent to --inputenc latin1 ---charset iso-8859-1. +.B \-latin1, \ \-\-latin1 +Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1 +\-\-charset iso\-8859\-1. .TP -.B -utf8, \ --utf8 -Select UTF-8 (Unicode) input files. It is equivalent to --inputenc -utf8 --charset utf-8. LATEX UTF-8 support can be found at -http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/. +.B \-utf8, \ \-\-utf8 +Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc +utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at +http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/. .TP -.BI --inputenc \ string +.BI \-\-inputenc \ string Give a LATEX input encoding, as an option to LATEX package inputenc. .TP -.BI --charset \ string +.BI \-\-charset \ string Specify the HTML character set, to be inserted in the HTML header. 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 , +for the Debian project (but may be used by others). diff --git a/man/coqmktop.1 b/man/coqmktop.1 index 3640d439..1b9c9e2a 100644 --- a/man/coqmktop.1 +++ b/man/coqmktop.1 @@ -17,10 +17,10 @@ coqmktop \- The Coq Proof Assistant user-tactics linker .B coqmktop builds a new Coq toplevel extended with user-tactics. .IR files \& -are the Objective Caml object or library files (i.e. with suffix .cmo, -.cmx, .cma or .cmxa) to link with the Coq system. +are the Objective Caml object or library files +(i.e. with suffix .cmo, .cmx, .cma or .cmxa) to link with the Coq system. The linker produces an executable Coq toplevel which can be called -directly or through coqc(1), using the -image option. +directly or through coqc(1), using the \-image option. .SH OPTIONS diff --git a/man/coqwc.1 b/man/coqwc.1 index 7011d148..4594aeec 100644 --- a/man/coqwc.1 +++ b/man/coqwc.1 @@ -44,4 +44,4 @@ Do not skip headers .SH BUGS Please report any bug to -.B coq-bugs@pauillac.inria.fr +.B coq\-bugs@pauillac.inria.fr diff --git a/man/parser.1 b/man/parser.1 deleted file mode 100644 index d89465d8..00000000 --- a/man/parser.1 +++ /dev/null @@ -1,30 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -parser \- Coq parser - - -.SH SYNOPSIS -.B parser -[ -.B options -] - -.SH DESCRIPTION - -.B parser -is a program reading Coq proof developments and outputing them in the -structured format given in the INRIA technical report RT154. This -program is not for the casual user. - -.SH SEE ALSO - -.BR coq-interface (1), -.BR coqc (1), -.BR coqtop (1), -.BR coqdep (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr -- cgit v1.2.3