diff options
-rw-r--r-- | doc/refman/coqdoc.tex | 14 | ||||
-rw-r--r-- | tools/coqdoc/main.ml | 4 |
2 files changed, 10 insertions, 8 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index ee2b042f4..30467a5e6 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -285,7 +285,7 @@ suffix \verb!.tex!. Select a \texmacs\ output. -\item[\texttt{--stdout}] ~\par +\item[\texttt{\mm{}stdout}] ~\par Write output to stdout. @@ -496,14 +496,16 @@ Default behavior is to assume ASCII 7 bits input files. \item[\texttt{-latin1}, \texttt{\mm{}latin1}] ~\par Select ISO-8859-1 input files. It is equivalent to - \texttt{--inputenc latin1 --charset iso-8859-1}. + \texttt{\mm{}inputenc latin1 \mm{}charset iso-8859-1}. \item[\texttt{-utf8}, \texttt{\mm{}utf8}] ~\par - Select UTF-8 (Unicode) input files. It is equivalent to - \texttt{--inputenc utf8 --charset utf-8}. - \LaTeX\ UTF-8 support can be found at - \url{http://www.ctan.org/pkg/unicode}. + Set \texttt{\mm{}inputenc utf8x} for \LaTeX\ output and + \texttt{\mm{}charset utf-8} for HTML output. Also use Unicode + replacements for a couple of standard plain ASCII notations such + as $\rightarrow$ for \texttt{->} and $\forall$ for + \texttt{forall}. \LaTeX\ UTF-8 support can be found at + \url{http://www.ctan.org/pkg/unicode}. \item[\texttt{\mm{}inputenc} \textit{string}] ~\par diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 2554ed495..22febd6a6 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -61,8 +61,8 @@ let usage () = prerr_endline " --coqlib_path <dir> set the path where Coq files are installed"; prerr_endline " -R <dir> <coqdir> map physical dir to Coq dir"; prerr_endline " -Q <dir> <coqdir> map physical dir to Coq dir"; - prerr_endline " --latin1 set ISO-8859-1 input language"; - prerr_endline " --utf8 set UTF-8 input language"; + prerr_endline " --latin1 set ISO-8859-1 mode"; + prerr_endline " --utf8 set UTF-8 mode"; prerr_endline " --charset <string> set HTML charset"; prerr_endline " --inputenc <string> set LaTeX input encoding"; prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module"; |