Imported Upstream version 8.1.pl3+dfsgupstream/8.1.pl3+dfsg

2 files changed, 27 insertions, 25 deletions

diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 28a0cd6d..2d0bc6c2 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 9976 2007-07-12 11:58:30Z msozeau $ i*)
+(*i $Id: output.ml 10248 2007-10-23 13:02:56Z notin $ i*)
 
 open Cdglobals
 open Index
@@ -41,8 +41,11 @@ let is_keyword =
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
       "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
-      "Unset"; "Variable"; "Variables"; 
-      "Notation"; 
+      "Set"; "Unset"; "Variable"; "Variables"; 
+      "Notation"; "Reserved Notation"; "Tactic Notation";
+      "Delimit"; "Bind"; "Open"; "Scope";
+      "Boxed"; "Unboxed";
+      "Arguments";
       (* Program *)
       "Program Definition"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -285,8 +288,8 @@ module Html = struct
     if !index && !current_module <> "Index" then 
       printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
     if !header_trailer then begin
-      printf "<hr/><font size=\"-1\">This page has been generated by ";
-      printf "<a href=\"%s\">coqdoc</a></font>\n" self;
+      printf "<hr/>This page has been generated by ";
+      printf "<a href=\"%s\">coqdoc</a>\n" self;
       printf "</div>\n\n</div>\n\n</body>\n</html>"
     end
 
@@ -420,9 +423,9 @@ module Html = struct
     let r = sprintf "%s.html#%s" !current_module lab in
     add_toc_entry (Toc_section (lev, f, r));
     stop_item ();
-    printf "<a name=\"%s\"></a><h%d>" lab lev;
+    printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev;
     f ();
-    printf "</h%d class=\"section\">\n" lev
+    printf "</h%d>\n" lev
 
   let rule () = printf "<hr/>\n"
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 2bf615d3..e16c7979 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 10074 2007-08-13 12:19:44Z notin $ i*)
+(*i $Id: pretty.mll 10248 2007-10-23 13:02:56Z notin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -224,7 +224,7 @@ let decl_token =
 
 let gallina_ext =
   "Module" 
-  | "Declare"
+  | "Declare" space+ "Module"
   | "Transparent"
   | "Opaque"
   | "Canonical"
@@ -327,25 +327,24 @@ rule coq_bol = parse
   | space* gallina_kw_to_hide
       { let s = lexeme lexbuf in
 	  if !light && section_or_end s then begin 
-	    skip_to_dot lexbuf; 
-	    coq_bol lexbuf 
-	  end else begin
-	    let s = lexeme lexbuf in 
-	    let nbsp = count_spaces s in
-	      indentation nbsp; 
-	      let s = String.sub s nbsp (String.length s - nbsp) in
-		ident s (lexeme_start lexbuf + nbsp); 
-		let eol= body lexbuf in 
-		  if eol then coq_bol lexbuf else coq lexbuf
-	  end }
+	      skip_to_dot lexbuf; 
+	      coq_bol lexbuf 
+	    end else begin
+		let nbsp = count_spaces s in
+		  indentation nbsp; 
+		  let s = String.sub s nbsp (String.length s - nbsp) in
+		    ident s (lexeme_start lexbuf + nbsp); 
+		    let eol= body lexbuf in 
+		      if eol then coq_bol lexbuf else coq lexbuf
+	      end }
   | space* gallina_kw
       { let s = lexeme lexbuf in 
-	let nbsp = count_spaces s in
+        let nbsp = count_spaces s in
+	let s = String.sub s nbsp (String.length s - nbsp)  in
 	  indentation nbsp;
-	  let s = String.sub s nbsp (String.length s - nbsp)  in
-	    ident s (lexeme_start lexbuf + nbsp); 
-	    let eol= body lexbuf in
-	      if eol then coq_bol lexbuf else coq lexbuf }
+	  ident s (lexeme_start lexbuf + nbsp); 
+	  let eol= body lexbuf in
+	    if eol then coq_bol lexbuf else coq lexbuf }
   | space* "(**" space+ "printing" space+ (identifier | token) space+
       { let tok = lexeme lexbuf in
 	let s = printing_token lexbuf in