Imported Upstream version 8.5~beta3+dfsg

3 files changed, 9 insertions, 7 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index cb704146..d2892167 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -320,6 +320,7 @@ let def_token =
   | "Instance"
   | "Declare" space+ "Instance"
   | "Global" space+ "Instance"
+  | "Functional" space+ "Scheme"
 
 let decl_token =
   "Hypothesis"
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 9531cd2b..22febd6a 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";
@@ -557,10 +557,8 @@ let produce_output fl =
 (*s \textbf{Main program.} Print the banner, parse the command line,
     read the files and then call [produce_document] from module [Web]. *)
 
-let main () =
+let _ =
   let files = parse () in
     Index.init_coqlib_library ();
     if not !quiet then banner ();
     if files <> [] then produce_output files
-
-let _ = Printexc.catch main ()
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 06030c45..8589f94a 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"