From d9fa3bb11966e69dc7734ebac678570c7732e74b Mon Sep 17 00:00:00 2001 From: glondu Date: Fri, 8 Aug 2008 14:44:12 +0000 Subject: Various fixes in manpages * hyphen meant as the ascii character should be escaped * lines starting with a dot have a special meaning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11322 85f007b7-540e-0410-9357-904b9bb8a0f7 --- man/coq-tex.1 | 22 +++++++++++----------- man/coqdep.1 | 10 +++++----- man/coqdoc.1 | 38 +++++++++++++++++++------------------- man/coqmktop.1 | 6 +++--- man/coqwc.1 | 2 +- man/parser.1 | 2 +- 6 files changed, 40 insertions(+), 40 deletions(-) (limited to 'man') diff --git a/man/coq-tex.1 b/man/coq-tex.1 index 737de70a9..7e0a2f81e 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 6ae89f8bd..e2cbb40e0 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 c443e8b04..45fcafd24 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/coqmktop.1 b/man/coqmktop.1 index 3640d439b..1b9c9e2a1 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 7011d1481..4594aeecb 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 index d89465d8c..051356b59 100644 --- a/man/parser.1 +++ b/man/parser.1 @@ -19,7 +19,7 @@ program is not for the casual user. .SH SEE ALSO -.BR coq-interface (1), +.BR coq\-interface (1), .BR coqc (1), .BR coqtop (1), .BR coqdep (1). -- cgit v1.2.3