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

6 files changed, 40 insertions, 40 deletions

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).