aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-10-02 16:01:46 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-10-02 16:01:46 +0200
commit16c88c9be5c37ee2e4fe04f7342365964031e7dd (patch)
tree7b5c07362dad323acae516718b9cebe94bd639af /tools
parenta3d7630d74b720b771e880dcf0fcad05de553a6e (diff)
parent88abc50ece70405d71777d5350ca2fa70c1ff437 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/main.ml4
-rw-r--r--tools/coqdoc/output.ml7
2 files changed, 7 insertions, 4 deletions
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";
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 06030c45a..8589f94a0 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -197,8 +197,11 @@ module Latex = struct
printf "\n";
printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n";
printf "%%interpret utf8 characters but extra packages might have to be added\n";
- printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n";
- printf "%%Use coqdoc's option -p to add new packages.\n";
+ printf "%%such as \"textgreek\" for Greek letters not already in tipa\n";
+ printf "%%or \"stmaryrd\" for mathematical symbols.\n";
+ printf "%%Utf8 codes missing a LaTeX interpretation can be defined by using\n";
+ printf "%%\\DeclareUnicodeCharacter{code}{interpretation}.\n";
+ printf "%%Use coqdoc's option -p to add new packages or declarations.\n";
printf "\\usepackage{tipa}\n";
printf "\n"