Update coqdoc documentation, CHANGES and add a fix for the proofbox (patch

by Chris Casinghino).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12311 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 23cc734738..31fb1453c9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -49,6 +49,23 @@ Tools
 - New coqtop/coqc option -compat X.Y to simulate the general behavior
   of previous versions of Coq (provides e.g. support for 8.2 compatibility).
 
+Coqdoc
+
+- List have been revamped.  List depth and scope is now determined by
+  an "offside" whitespace rule.
+- Text may be italicized by placing it in _underscores_.
+- The "--index <string>" flag changes the filename of the index.
+- The "--toc-depth <int>" flag limits the depth of headers which are
+  included in the table of contents.
+- The "--lib-name <string>" flag prints "<string> Foo" instead of
+  "Library Foo" where library titles are called for.  The
+  "--no-lib-name" flag eliminates the extra title.
+- New option "--parse-comments" to allow parsing of regular ("(* *)") 
+  comments.
+- New option "--plain-comments" to disable interpretation inside comments.
+- New option "--interpolate" to try and typeset identifiers in Coq escapings
+  using the available globalization information.
+
 Library
 
 - Use "Coq standard" names for the properties of eq and identity