diff options
Diffstat (limited to 'man/coqdoc.1')
| -rw-r--r-- | man/coqdoc.1 | 38 |
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. |