aboutsummaryrefslogtreecommitdiff
path: root/tools/coqdoc
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc')
-rw-r--r--tools/coqdoc/alpha.ml2
-rw-r--r--tools/coqdoc/alpha.mli2
-rw-r--r--tools/coqdoc/cdglobals.ml2
-rw-r--r--tools/coqdoc/cpretty.mli2
-rw-r--r--tools/coqdoc/cpretty.mll3
-rw-r--r--tools/coqdoc/index.ml2
-rw-r--r--tools/coqdoc/index.mli2
-rw-r--r--tools/coqdoc/main.ml6
-rw-r--r--tools/coqdoc/output.ml9
-rw-r--r--tools/coqdoc/output.mli2
-rw-r--r--tools/coqdoc/tokens.ml2
-rw-r--r--tools/coqdoc/tokens.mli2
12 files changed, 20 insertions, 16 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index 46005741da..f6d47a55de 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index de7290a440..5d48473d8c 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 4e132ba03d..58b19184e7 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index cb70414675..431080c6bc 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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/index.ml b/tools/coqdoc/index.ml
index 4a5ff59245..47acc7b436 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 69b4e4daea..e44bbd593a 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 2554ed495b..fe4387381d 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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 06030c45a6..2b2690968d 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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"
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index c4628dd846..853bc29aa4 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index a93ae85579..b6a1057aa8 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index c4fe3bc8f3..f07efedf9e 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-01 09:14:22 +0000