From 5481ff4f6935874ac3798a61f5a2a810006bde37 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Sep 2015 15:00:33 +0200 Subject: Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015. --- tools/coqdoc/main.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tools/coqdoc') diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 2554ed495b..22febd6a64 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -61,8 +61,8 @@ let usage () = prerr_endline " --coqlib_path set the path where Coq files are installed"; prerr_endline " -R map physical dir to Coq dir"; prerr_endline " -Q 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 set HTML charset"; prerr_endline " --inputenc set LaTeX input encoding"; prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module"; -- cgit v1.2.3 From 4b88d774729e0ab7916730e8e6ebedc2033a87f2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Sep 2015 16:31:29 +0200 Subject: Documenting how to support some special unicode characters in coqdoc (thanks to coq-club, Sep 2015). --- tools/coqdoc/output.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'tools/coqdoc') diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 06030c45a6..8589f94a01 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" -- cgit v1.2.3 From d30a7244b52e86c364320a8fa0794c7686f30074 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 23 Oct 2015 07:45:15 +0200 Subject: Support "Functional Scheme" in coqdoc. (Fix bug #4382) --- tools/coqdoc/cpretty.mll | 1 + 1 file changed, 1 insertion(+) (limited to 'tools/coqdoc') diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index cb70414675..d28921674b 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" -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- tools/coqdoc/alpha.ml | 2 +- tools/coqdoc/alpha.mli | 2 +- tools/coqdoc/cdglobals.ml | 2 +- tools/coqdoc/cpretty.mli | 2 +- tools/coqdoc/cpretty.mll | 2 +- tools/coqdoc/index.ml | 2 +- tools/coqdoc/index.mli | 2 +- tools/coqdoc/main.ml | 2 +- tools/coqdoc/output.ml | 2 +- tools/coqdoc/output.mli | 2 +- tools/coqdoc/tokens.ml | 2 +- tools/coqdoc/tokens.mli | 2 +- 12 files changed, 12 insertions(+), 12 deletions(-) (limited to 'tools/coqdoc') diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml index c3db3a265d..f817ed5a2a 100644 --- a/tools/coqdoc/alpha.ml +++ b/tools/coqdoc/alpha.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*