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

3 files changed, 13 insertions, 2 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 3ad900050..065b72e7b 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -780,7 +780,7 @@ and doc indents = parse
 		  | None -> doc_bol lexbuf
 		else doc indents lexbuf)}
   | "[]"
-      { Output.symbol "PROOFBOX"; doc indents lexbuf }
+      { Output.proofbox (); doc indents lexbuf }
   | "["
       { if !Cdglobals.plain_comments then Output.char '['
         else (brackets := 1;  Output.start_inline_coq (); escaped_coq lexbuf;
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 11a821b7c..b2e6bbd99 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -131,7 +131,6 @@ let initialize () =
 	"exists", "\\ensuremath{\\exists}", if_utf8 "∃";
 	"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
 	"λ", "\\ensuremath{\\lambda}", if_utf8 "λ";
-      "PROOFBOX", "\\ensuremath{\\Box}", Some "<font size=-2>&#9744;</font>"; (* FIX THIS *)
 	(* "fun", "\\ensuremath{\\lambda}" ? *)
       ]
 
@@ -318,6 +317,8 @@ module Latex = struct
     
   let symbol s = with_latex_printing raw_ident s
 
+  let proofbox () = printf "\\ensuremath{\\Box}"
+
   let rec reach_item_level n = 
     if !item_level < n then begin
       printf "\n\\begin{itemize}\n\\item "; incr item_level;
@@ -548,6 +549,8 @@ module Html = struct
   let symbol s =
     with_html_printing raw_ident s
 
+  let proofbox () = printf "<font size=-2>&#9744;</font>"
+
   let rec reach_item_level n = 
     if !item_level < n then begin
       printf "<ul>\n<li>"; incr item_level;
@@ -810,6 +813,8 @@ module TeXmacs = struct
 
   let symbol s = if !in_doc then symbol_true s else raw_ident s
 
+  let proofbox () = printf "QED"
+
   let rec reach_item_level n = 
     if !item_level < n then begin
       printf "\n<\\itemize>\n<item>"; incr item_level;
@@ -921,6 +926,8 @@ module Raw = struct
 
   let symbol s = raw_ident s
 
+  let proofbox () = printf "[]"
+
   let item n = printf "- "
   let stop_item () = ()
   let reach_item_level _ = ()
@@ -1017,6 +1024,8 @@ let char = select Latex.char Html.char TeXmacs.char Raw.char
 let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
 let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol
 
+let proofbox = select Latex.proofbox Html.proofbox TeXmacs.proofbox Raw.proofbox
+
 let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.latex_char
 let latex_string = 
   select Latex.latex_string Html.latex_string TeXmacs.latex_string Raw.latex_string
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 6e3f6e88b..35f056d94 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -61,6 +61,8 @@ val char : char -> unit
 val ident : string -> loc -> unit
 val symbol : string -> unit
 
+val proofbox : unit -> unit
+
 val latex_char : char -> unit
 val latex_string : string -> unit
 val html_char : char -> unit