summaryrefslogtreecommitdiff
path: root/man/coqdoc.1
diff options
context:
space:
mode:
Diffstat (limited to 'man/coqdoc.1')
-rw-r--r--man/coqdoc.138
1 files changed, 19 insertions, 19 deletions
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.