13 files changed, 593 insertions, 233 deletions

diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index 83bfa5ed..8802c0ef 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: alpha.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Cdglobals
 
 let norm_char_latin1 c = match Char.uppercase c with
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index ec5b084f..792b71fc 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: alpha.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (* Alphabetic order. *)
 
 val compare_char : char -> char -> int
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5cb670dc..f37db46b 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-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -49,21 +49,40 @@ type glob_source_t =
 
 let glob_source = ref DotGlob
 
+(*s Manipulations of paths and path aliases *)
+
+let normalize_path p =
+  (* We use the Unix subsystem to normalize a physical path (relative
+     or absolute) and get rid of symbolic links, relative links (like
+     ./ or ../ in the middle of the path; it's tricky but it
+     works... *)
+  (* Rq: Sys.getcwd () returns paths without '/' at the end *)
+  let orig = Sys.getcwd () in
+  Sys.chdir p;
+  let res = Sys.getcwd () in
+  Sys.chdir orig;
+  res
+
+let normalize_filename f =
+  let basename = Filename.basename f in
+  let dirname = Filename.dirname f in
+  normalize_path dirname, basename
+
 (** A weaker analog of the function in Envars *)
 
 let guess_coqlib () =
   let file = "states/initial.coq" in
-  if Sys.file_exists (Filename.concat Coq_config.coqlib file)
-  then Coq_config.coqlib
-  else
-    let coqbin = Filename.dirname Sys.executable_name in
-    let prefix = Filename.dirname coqbin in
-    let rpath = if Coq_config.local then [] else
-	(if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
-    let coqlib = List.fold_left Filename.concat prefix rpath in
-    if Sys.file_exists (Filename.concat coqlib file) then coqlib
-    else
-      Coq_config.coqlib
+  match Coq_config.coqlib with
+    | Some coqlib when Sys.file_exists (Filename.concat coqlib file) ->
+      coqlib
+    | Some _ | None ->
+      let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
+      let prefix = Filename.dirname coqbin in
+      let rpath = if Coq_config.local then [] else
+	  (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
+      let coqlib = List.fold_left Filename.concat prefix rpath in
+      if Sys.file_exists (Filename.concat coqlib file) then coqlib
+      else prefix
 
 let header_trailer = ref true
 let header_file = ref ""
@@ -90,6 +109,7 @@ let toc_depth = (ref None : int option ref)
 let lib_name = ref "Library"
 let lib_subtitles = ref false
 let interpolate = ref false
+let inline_notmono = ref false
 
 let charset = ref "iso-8859-1"
 let inputenc = ref ""
@@ -103,7 +123,7 @@ let set_latin1 () =
 
 let set_utf8 () =
   charset := "utf-8";
-  inputenc := "utf8";
+  inputenc := "utf8x";
   utf8 := true
 
 (* Parsing options *)
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index 24b514b7..ccd285f1 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -101,8 +101,13 @@ h4.section {
     color: rgb(30%,30%,70%);
     font-family: monospace } 
 
-.doc .inlinecode .id {
-    color: rgb(30%,30%,70%);
+.doc .inlinecode .id { 
+    color: rgb(30%,30%,70%); 
+} 
+
+.inlinecodenm { 
+    display: inline;
+    color: #444444;
 }
 
 .doc .code { 
@@ -124,6 +129,32 @@ h4.section {
     font-family: monospace;
  } 
 
+table.infrule {
+  border: 0px;
+  margin-left: 50px;
+  margin-top: 10px;
+  margin-bottom: 10px;
+}
+
+td.infrule {
+    font-family: monospace;
+    text-align: center;
+/*    color: rgb(35%,35%,70%);  */
+    padding: 0px;
+    line-height: 100%;
+}
+
+tr.infrulemiddle hr {
+    margin: 1px 0 1px 0;
+}
+
+.infrulenamecol {
+    color: rgb(60%,60%,60%); 
+    font-size: 80%;
+    padding-left: 1em;
+    padding-bottom: 0.1em
+}
+
 /* Pied de page */
 
 #footer { font-size: 65%;
@@ -231,4 +262,13 @@ h4.section {
     position: absolute;
     bottom: 0;
     text-align: bottom;
-}
\ No newline at end of file
+}
+
+.paragraph {
+    height: 0.75em;
+}
+
+ul.doclist {
+    margin-top: 0em;
+    margin-bottom: 0em;
+}
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 085ae122..adc49ed4 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cpretty.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Index
 
 val coq_file : string -> Cdglobals.coq_module -> unit
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index a2bcb987..d7b54fd0 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cpretty.mll 14868 2011-12-26 17:07:24Z herbelin $ i*)
-
 (*s Utility functions for the scanners *)
 
 {
@@ -80,8 +77,17 @@
   let in_proof = ref None
   let in_emph = ref false
 
-  let start_emph () = in_emph := true; Output.start_emph ()
-  let stop_emph () = if !in_emph then (Output.stop_emph (); in_emph := false)
+  let in_env start stop = 
+    let r = ref false in
+    let start_env () = r := true; start () in
+    let stop_env () = if !r then stop (); r := false in
+      (fun x -> !r), start_env, stop_env
+      
+  let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
+  let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote
+
+  let url_buffer = Buffer.create 40
+  let url_name_buffer = Buffer.create 40
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
     lexbuf.lex_curr_p <- lexbuf.lex_start_p
@@ -257,7 +263,7 @@
     let nbsp,isp = count_spaces s in
     Output.indentation nbsp;
     let s = String.sub s isp (String.length s - isp) in
-    Output.ident s (lexeme_start lexbuf + isp)
+    Output.keyword s (lexeme_start lexbuf + isp)
 
 }
 
@@ -323,6 +329,7 @@ let def_token =
   | "SubClass"
   | "Example"
   | "Fixpoint"
+  | "Function"
   | "Boxed"
   | "CoFixpoint"
   | "Record"
@@ -371,13 +378,17 @@ let commands =
   | "Drop"
   | "ProtectedLoop"
   | "Quit"
+  | "Restart"
   | "Load"
   | "Add"
   | "Remove" space+ "Loadpath"
   | "Print"
   | "Inspect"
   | "About"
+  | "SearchAbout"
+  | "SearchRewrite"
   | "Search"
+  | "Locate"
   | "Eval"
   | "Reset"
   | "Check"
@@ -405,6 +416,14 @@ let prog_kw =
   | "Obligations"
   | "Solve"
 
+let hint_kw = 
+  "Extern" | "Rewrite" | "Resolve" | "Immediate" | "Transparent" | "Opaque" | "Unfold" | "Constructors"
+
+let set_kw =
+    "Printing" space+ ("Coercions" | "Universes" | "All")
+  | "Implicit" space+ "Arguments"
+  
+
 let gallina_kw_to_hide =
     "Implicit" space+ "Arguments"
   | "Ltac"
@@ -412,15 +431,16 @@ let gallina_kw_to_hide =
   | "Import"
   | "Export"
   | "Load"
-  | "Hint"
+  | "Hint" space+ hint_kw
   | "Open"
   | "Close"
   | "Delimit"
   | "Transparent"
   | "Opaque"
   | ("Declare" space+ ("Morphism" | "Step") )
-  | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+  | ("Set" | "Unset") space+ set_kw
   | "Declare" space+ ("Left" | "Right") space+ "Step"
+  | "Debug" space+ ("On" | "Off")
 
 
 let section = "*" | "**" | "***" | "****"
@@ -512,7 +532,7 @@ rule coq_bol = parse
 	output_indented_keyword s lexbuf;
 	let eol= body lexbuf in
 	if eol then coq_bol lexbuf else coq lexbuf }
-  | space* notation_kw space*
+  | space* notation_kw
       {	let s = lexeme lexbuf in
 	output_indented_keyword s lexbuf;
 	let eol= start_notation_string lexbuf in
@@ -639,7 +659,7 @@ and coq = parse
 	  Output.ident s (lexeme_start lexbuf);
 	let eol = body lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
-  | notation_kw space*
+  | notation_kw
       { let s = lexeme lexbuf in
 	Output.ident s (lexeme_start lexbuf);
 	let eol= start_notation_string lexbuf in
@@ -663,8 +683,6 @@ and coq = parse
 (*s Scanning documentation, at beginning of line *)
 
 and doc_bol = parse
-  | space* nl+
-      { Output.paragraph (); doc_bol lexbuf }
   | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
       { let eol, lex = strip_eol (lexeme lexbuf) in
         let lev, s = sec_title lex in
@@ -674,33 +692,26 @@ and doc_bol = parse
           else
             Output.section lev (fun () -> ignore (doc None (from_string s)));
 	    if eol then doc_bol lexbuf else doc None lexbuf }
-  | space* nl space* '-'+
-      { (* adding this production instead of just letting the paragraph
-           production and the begin list production fire eliminates
-           extra vertical whitespace. *)
-        let buf' = lexeme lexbuf in
-        let buf =
-          let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
-            match bufs with
-              | (_ :: s :: []) -> s
-              | (_ :: _ :: s :: _) -> s
-              | _ -> eprintf "Internal error bad_split1 - please report\n";
-                     exit 1
+  | space_nl* '-'+
+      { let buf' = lexeme lexbuf in
+        let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
+        let lines = (List.length bufs) - 1 in
+        let line = 
+          match bufs with
+          | [] -> eprintf "Internal error bad_split1 - please report\n";
+                  exit 1
+          | _ -> List.nth bufs lines
         in
-          match check_start_list buf with
+          match check_start_list line with
           | Neither -> backtrack_past_newline lexbuf; doc None lexbuf
-          | List n -> Output.item 1; doc (Some [n]) lexbuf
-          | Rule -> Output.rule (); doc None lexbuf
-      }
-  | space* '-'+
-      { let buf = lexeme lexbuf in
-          match check_start_list buf with
-          | Neither -> backtrack lexbuf; doc None lexbuf
-          | List n -> Output.item 1; doc (Some [n]) lexbuf
+          | List n -> Output.paragraph ();
+                      Output.item 1; doc (Some [n]) lexbuf
           | Rule -> Output.rule (); doc None lexbuf
       }
+  | space* nl+
+      { Output.paragraph (); doc_bol lexbuf }
   | "<<" space*
-      { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
+      { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf }
   | eof
       { true }
   | '_'
@@ -724,8 +735,8 @@ and doc_list_bol indents = parse
             backtrack lexbuf; doc_bol lexbuf
       }
   | "<<" space*
-      { Output.start_verbatim ();
-        verbatim lexbuf;
+      { Output.start_verbatim false;
+        verbatim false lexbuf;
         doc_list_bol indents lexbuf }
   | "[[" nl
       { formatted := true;
@@ -734,6 +745,8 @@ and doc_list_bol indents = parse
         Output.end_inline_coq_block ();
         formatted := false;
         doc_list_bol indents lexbuf }
+  | "[[[" nl
+      { inf_rules (Some indents) lexbuf }
   | space* nl space* '-'
       { (* Like in the doc_bol production, these two productions
            exist only to deal properly with whitespace *)
@@ -769,9 +782,16 @@ and doc_list_bol indents = parse
                 backtrack_past_newline lexbuf;
                 doc_list_bol indents lexbuf
               end
-        | Before -> Output.stop_item ();
-                    backtrack_past_newline lexbuf;
-                    doc_bol lexbuf
+        | Before -> 
+        (* Here we were at the beginning of a line, and it was blank.
+           The next line started before any list items.  So: insert
+           a paragraph for the empty line, rewind to whatever's just
+           after the newline, then toss over to doc_bol for whatever
+           comes next. *)
+            Output.stop_item ();
+            Output.paragraph ();
+            backtrack_past_newline lexbuf;
+            doc_bol lexbuf
 
       }
   | space* _
@@ -780,7 +800,10 @@ and doc_list_bol indents = parse
         | Before -> Output.stop_item (); backtrack lexbuf;
                     doc_bol lexbuf
         | StartLevel n ->
-            Output.reach_item_level (n-1);
+            (if n = 1 then
+               Output.stop_item ()
+             else
+               Output.reach_item_level (n-1));
             backtrack lexbuf;
             doc (Some (take (n-1) indents)) lexbuf
         | InLevel (n,_) ->
@@ -808,8 +831,11 @@ and doc indents = parse
 		  | Some ls -> doc_list_bol ls lexbuf
 		  | None -> doc_bol lexbuf
 		else doc indents lexbuf)}
+  | "[[[" nl
+      { inf_rules indents lexbuf }
   | "[]"
       { Output.proofbox (); doc indents lexbuf }
+  | "{{" { url lexbuf; doc indents lexbuf }
   | "["
       { if !Cdglobals.plain_comments then Output.char '['
         else (brackets := 1;  Output.start_inline_coq (); escaped_coq lexbuf;
@@ -823,6 +849,18 @@ and doc indents = parse
         let eol = comment lexbuf in
           if eol then bol_parse lexbuf else doc indents lexbuf
       }
+  | '*'* "*)" space_nl* "(**"
+      {(match indents with
+        | Some _ -> Output.stop_item ()
+        | None -> ());
+       (* this says - if there is a blank line between the two comments,
+          insert one in the output too *)
+       let lines = List.length (Str.split_delim (Str.regexp "['\n']") 
+                                                (lexeme lexbuf))
+       in 
+         if lines > 2 then Output.paragraph ();
+       doc_bol lexbuf
+      }
   | '*'* "*)" space* nl
       { true }
   | '*'* "*)"
@@ -857,6 +895,15 @@ and doc indents = parse
       { if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ;
         Output.char (lexeme_char lexbuf 1);
         doc indents lexbuf }
+  | "<<" space*
+      { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf }
+  | '"'
+      { if !Cdglobals.plain_comments 
+	then Output.char '"' 
+	else if in_quote ()
+	then stop_quote () 
+	else start_quote ();
+        doc indents lexbuf }
   | eof
       { false }
   | _
@@ -883,11 +930,22 @@ and escaped_html = parse
   | eof { () }
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
-and verbatim = parse
-  | nl ">>" space* nl { Output.verbatim_char '\n'; Output.stop_verbatim () }
-  | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
-  | eof { Output.stop_verbatim () }
-  | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
+and verbatim inline = parse
+  | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
+  | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
+  | ">>" { Output.stop_verbatim inline }
+  | eof { Output.stop_verbatim inline }
+  | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
+
+and url = parse
+  | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }
+  | "}" { url_name lexbuf }
+  | _ { Buffer.add_char url_buffer (lexeme_char lexbuf 0); url lexbuf }
+
+and url_name = parse
+  | "}" { Output.url (Buffer.contents url_buffer) (Some (Buffer.contents url_name_buffer));
+	  Buffer.clear url_buffer; Buffer.clear url_name_buffer }
+  | _ { Buffer.add_char url_name_buffer (lexeme_char lexbuf 0); url_name lexbuf }
 
 (*s Coq, inside quotations *)
 
@@ -911,10 +969,16 @@ and escaped_coq = parse
       { Tokens.flush_sublexer();
         Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
         escaped_coq lexbuf }
-  | space
-      { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
-        escaped_coq lexbuf }
-  | _
+  | space_nl*
+      { let str = lexeme lexbuf in
+          Tokens.flush_sublexer();
+          (if !Cdglobals.inline_notmono then () 
+                                        else Output.end_inline_coq ()); 
+          String.iter Output.char str; 
+          (if !Cdglobals.inline_notmono then () 
+                                        else Output.start_inline_coq ());
+          escaped_coq lexbuf }
+  | _ 
       { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf);
         escaped_coq lexbuf }
 
@@ -1081,7 +1145,7 @@ and body = parse
 	     if eol
 	     then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
 	     else body lexbuf }
-  | "where" space*
+  | "where" 
       { Tokens.flush_sublexer();
         Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
 	start_notation_string lexbuf }
@@ -1105,6 +1169,8 @@ and body = parse
         body lexbuf }
 
 and start_notation_string = parse
+  | space { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
+	    start_notation_string lexbuf }
   | '"' (* a true notation *)
       { Output.sublexer '"' (lexeme_start lexbuf);
         notation_string lexbuf;
@@ -1141,6 +1207,71 @@ and printing_token_body = parse
   | _   { Buffer.add_string token_buffer (lexeme lexbuf);
 	  printing_token_body lexbuf }
 
+(*s These handle inference rules, parsing the body segments of things
+    enclosed in [[[  ]]] brackets *)
+and inf_rules indents = parse
+  | space* nl     (* blank line, before or between definitions *)
+      { inf_rules indents lexbuf }
+  | "]]]" nl      (* end of the inference rules block *)
+      { match indents with
+        | Some ls -> doc_list_bol ls lexbuf
+        | None -> doc_bol lexbuf }
+  | _ 
+      { backtrack lexbuf;  (* anything else must be the first line in a rule *)
+        inf_rules_assumptions indents [] lexbuf}
+
+(* The inference rule parsing just collects the inference rule and then
+   calls the output function once, instead of doing things incrementally
+   like the rest of the lexer.  If only there were a real parsing phase...
+*)
+and inf_rules_assumptions indents assumptions = parse
+  | space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *)
+      { let line = lexeme lexbuf in
+        let (spaces,_) = count_spaces line in
+        let dashes_and_name = 
+               cut_head_tail_spaces (String.sub line 0 (String.length line - 1))
+        in
+        let ldn = String.length dashes_and_name in
+        let (dashes,name) = 
+          try (let i = String.index dashes_and_name ' ' in
+               let d = String.sub dashes_and_name 0 i in
+               let n = cut_head_tail_spaces 
+                        (String.sub dashes_and_name (i+1) (ldn-i-1))
+               in
+                 (d, Some n))
+          with _ -> (dashes_and_name, None)
+            
+        in
+          inf_rules_conclusion indents (List.rev assumptions) 
+                               (spaces, dashes, name) [] lexbuf }
+  | [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *)
+      { let line = lexeme lexbuf in
+        let (spaces,_) = count_spaces line in
+        let assumption = cut_head_tail_spaces 
+                            (String.sub line 0 (String.length line - 1))
+        in
+          inf_rules_assumptions indents ((spaces,assumption)::assumptions)
+                                lexbuf }
+
+(*s The conclusion is required to come immediately after the
+    horizontal bar.  It is allowed to contain multiple lines of
+    text, like the assumptions.  The conclusion ends when we spot a
+    blank line or a ']]]'. *)
+and inf_rules_conclusion indents assumptions middle conclusions = parse
+  | space* nl | space* "]]]" nl (* end of conclusions. *)
+      { backtrack lexbuf;
+        Output.inf_rule assumptions middle (List.rev conclusions);
+        inf_rules indents lexbuf }
+  | space* [^ '\n']+ nl (* this is a line in the conclusion *)
+      { let line = lexeme lexbuf in
+        let (spaces,_) = count_spaces line in
+        let conc = cut_head_tail_spaces (String.sub line 0 
+                                                    (String.length line - 1))
+        in
+          inf_rules_conclusion indents assumptions middle 
+                               ((spaces,conc) :: conclusions) lexbuf
+      }
+
 (*s A small scanner to support the chapter subtitle feature *)
 and st_start m = parse
   | "(*" "*"+ space+ "*" space+
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index a2cb995e..14447b06 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Filename
 open Lexing
 open Printf
@@ -38,17 +35,18 @@ type entry_type =
 type index_entry =
   | Def of string * entry_type
   | Ref of coq_module * string * entry_type
-  | Mod of coq_module * string
 
 let current_type : entry_type ref = ref Library
 let current_library = ref ""
   (** refers to the file being parsed *)
 
-(** [deftable] stores only definitions and is used to interpolate idents
-    inside comments, which are not globalized otherwise. *)
-
+(** [deftable] stores only definitions and is used to build the index *)
 let deftable = Hashtbl.create 97
 
+(** [byidtable] is used to interpolate idents inside comments, which are not
+    globalized otherwise. *)
+let byidtable = Hashtbl.create 97
+
 (** [reftable] stores references and definitions *)
 let reftable = Hashtbl.create 97
 
@@ -62,25 +60,25 @@ let full_ident sp id =
   else ""
 
 let add_def loc1 loc2 ty sp id =
+  let fullid = full_ident sp id in
+  let def = Def (fullid, ty) in
   for loc = loc1 to loc2 do
-    Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty))
+    Hashtbl.add reftable (!current_library, loc) def
   done;
-  Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
+  Hashtbl.add deftable !current_library (fullid, ty);
+  Hashtbl.add byidtable id (!current_library, fullid, ty)
 
 let add_ref m loc m' sp id ty =
+  let fullid = full_ident sp id in
   if Hashtbl.mem reftable (m, loc) then ()
-  else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
+  else Hashtbl.add reftable (m, loc) (Ref (m', fullid, ty));
   let idx = if id = "<>" then m' else id in
-    if Hashtbl.mem deftable idx then ()
-    else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
-
-let add_mod m loc m' id =
-  Hashtbl.add reftable (m, loc) (Mod (m', id));
-  Hashtbl.add deftable m (Mod (m', id))
+    if Hashtbl.mem byidtable idx then ()
+    else Hashtbl.add byidtable idx (m', fullid, ty)
 
 let find m l = Hashtbl.find reftable (m, l)
 
-let find_string m s = Hashtbl.find deftable s
+let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
 
 (*s Manipulating path prefixes *)
 
@@ -238,18 +236,20 @@ let type_name = function
 let prepare_entry s = function
   | Notation ->
       (* We decode the encoding done in Dumpglob.cook_notation of coqtop *)
-      (* Encoded notations have the form section:sc:x_'++'_x where: *)
-      (* - the section, if any, ends with a "." *)
-      (* - the scope can be empty *)
-      (* - tokens are separated with "_" *)
-      (* - non-terminal symbols are conventionally represented by "x" *)
-      (* - terminals are enclosed within simple quotes *)
-      (* - existing simple quotes (that necessarily are parts of terminals) *)
-      (*   are doubled *)
+      (* Encoded notations have the form section:sc:x_'++'_x where:      *)
+      (* - the section, if any, ends with a "."                          *)
+      (* - the scope can be empty                                        *)
+      (* - tokens are separated with "_"                                 *)
+      (* - non-terminal symbols are conventionally represented by "x"    *)
+      (* - terminals are enclosed within simple quotes                   *)
+      (* - existing simple quotes (that necessarily are parts of         *)
+      (*   terminals) are doubled                                        *)
       (*   (as a consequence, when a terminal contains "_" or "x", these *)
       (*   necessarily appear enclosed within non-doubled simple quotes) *)
-      (*   Example: "x ' %x _% y %'x %'_' z" is encoded as *)
-      (*     "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x" *)
+      (* - non-printable characters < 32 are left encoded so that they   *)
+      (*   are human-readable in index files                             *)
+      (* Example: "x ' %x _% y %'x %'_' z" is encoded as                 *)
+      (*   "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x"                        *)
       let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in
       let h = try String.index_from s 0 ':' with _ -> err () in
       let i = try String.index_from s (h+1) ':' with _ -> err () in
@@ -268,10 +268,10 @@ let prepare_entry s = function
 	  | _ -> assert false)
 	end
 	else
-	  if s.[!j] = '\'' then begin
-	    if (!j = l || s.[!j+1] <> '\'') then quoted := false
-	    else (ntn.[!k] <- s.[!j]; incr k; incr j)
-	  end else begin
+	  if s.[!j] = '\'' then
+	    if (!j = l || s.[!j+1] = '_') then quoted := false
+	    else (incr j; ntn.[!k] <- s.[!j]; incr k)
+	  else begin
 	    ntn.[!k] <- s.[!j];
 	    incr k
 	  end;
@@ -290,11 +290,8 @@ let all_entries () =
     let l = try Hashtbl.find bt t with Not_found -> [] in
       Hashtbl.replace bt t ((s,m) :: l)
   in
-  let classify (m,_) e = match e with
-    | Def (s,t) -> add_g s m t; add_bt t s m
-    | Ref _ | Mod _ -> ()
-  in
-    Hashtbl.iter classify reftable;
+  let classify m (s,t) = (add_g s m t; add_bt t s m) in
+    Hashtbl.iter classify deftable;
     Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
     { idx_name = "global";
       idx_entries = sort_entries !gl;
@@ -324,8 +321,27 @@ let type_of_string = function
   | "sec" -> Section
   | s -> raise (Invalid_argument ("type_of_string:" ^ s))
 
-let read_glob f =
+let ill_formed_glob_file f =
+  eprintf "Warning: ill-formed file %s (links will not be available)\n" f
+let outdated_glob_file f =
+  eprintf "Warning: %s not consistent with corresponding .v file (links will not be available)\n" f
+
+let correct_file vfile f c =
+  let s = input_line c in
+  if String.length s < 7 || String.sub s 0 7 <> "DIGEST " then
+    (ill_formed_glob_file f; false)
+  else
+    let s = String.sub s 7 (String.length s - 7) in
+    match vfile, s with
+    | None, "NO" -> true
+    | Some _, "NO" -> ill_formed_glob_file f; false
+    | None, _ -> ill_formed_glob_file f; false
+    | Some vfile, s ->
+        s = Digest.to_hex (Digest.file vfile) || (outdated_glob_file f; false)
+
+let read_glob vfile f =
   let c = open_in f in
+  if correct_file vfile f c then
   let cur_mod = ref "" in
   try
     while true do
@@ -341,7 +357,16 @@ let read_glob f =
 		Scanf.sscanf s "R%d:%d %s %s %s %s"
 		  (fun loc1 loc2 lib_dp sp id ty ->
 		    for loc=loc1 to loc2 do
-		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty)
+		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty);
+
+                      (* Also add an entry for each module mentioned in [lib_dp],
+                       * to use in interpolation. *)
+                      ignore (List.fold_right (fun thisPiece priorPieces ->
+                                                let newPieces = match priorPieces with
+                                                                | "" -> thisPiece
+                                                                | _ -> thisPiece ^ "." ^ priorPieces in
+                                                add_ref !cur_mod loc "" "" newPieces Library;
+                                                newPieces) (Str.split (Str.regexp_string ".") lib_dp) "")
 		    done)
 	       with _ -> ())
 	  | _ ->
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index a009e9dc..0f62a086 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Cdglobals
 
 type loc = int
@@ -36,10 +34,11 @@ val type_name : entry_type -> string
 type index_entry =
   | Def of string * entry_type
   | Ref of coq_module * string * entry_type
-  | Mod of coq_module * string
 
+(* Find what symbol coqtop said is located at loc in the source file *)
 val find : coq_module -> loc -> index_entry
 
+(* Find what data is referred to by some string in some coq module *)
 val find_string : coq_module -> string -> index_entry
 
 val add_module : coq_module -> unit
@@ -54,7 +53,7 @@ val add_external_library : string -> coq_module -> unit
 
 (*s Read globalizations from a file (produced by coqc -dump-glob) *)
 
-val read_glob : string -> unit
+val read_glob : Digest.t option -> string -> unit
 
 (*s Indexes *)
 
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 23dadbc1..b33ec1f0 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
  *  - coq_module: chop ./// (arbitrary amount of slashes), not only "./"
@@ -53,6 +50,7 @@ let usage () =
   prerr_endline "  -p <string>          insert <string> in LaTeX preamble";
   prerr_endline "  --files-from <file>  read file names to process in <file>";
   prerr_endline "  --glob-from <file>   read globalization information from <file>";
+  prerr_endline "  --no-glob            don't use any globalization information (no links will be inserted at identifiers)";
   prerr_endline "  --quiet              quiet mode (default)";
   prerr_endline "  --verbose            verbose mode";
   prerr_endline "  --no-externals       no links to Coq standard library";
@@ -73,6 +71,7 @@ let usage () =
   prerr_endline "  --no-lib-name        don't display \"Library\" before library names in the toc";
   prerr_endline "  --lib-name <string>  call top level toc entries <string> instead of \"Library\"";
   prerr_endline "  --lib-subtitles      first line comments of the form (** * ModuleName : text *) will be interpreted as subtitles";
+  prerr_endline "  --inline-notmono     use a proportional width font for inline code (possibly with a different color)";
   prerr_endline "";
   exit 1
 
@@ -107,25 +106,6 @@ let check_if_file_exists f =
   end
 
 
-(*s Manipulations of paths and path aliases *)
-
-let normalize_path p =
-  (* We use the Unix subsystem to normalize a physical path (relative
-     or absolute) and get rid of symbolic links, relative links (like
-     ./ or ../ in the middle of the path; it's tricky but it
-     works... *)
-  (* Rq: Sys.getcwd () returns paths without '/' at the end *)
-  let orig = Sys.getcwd () in
-  Sys.chdir p;
-  let res = Sys.getcwd () in
-  Sys.chdir orig;
-  res
-
-let normalize_filename f =
-  let basename = Filename.basename f in
-  let dirname = Filename.dirname f in
-  normalize_path dirname, basename
-
 (* [paths] maps a physical path to a name *)
 let paths = ref []
 
@@ -303,6 +283,9 @@ let parse () =
     | ("-lib-subtitles" | "--lib-subtitles") :: rem ->
       Cdglobals.lib_subtitles := true;
       parse_rec rem
+    | ("-inline-notmono" | "--inline-notmono") :: rem ->
+      Cdglobals.inline_notmono := true;
+      parse_rec rem
 
     | ("-latin1" | "--latin1") :: rem ->
 	Cdglobals.set_latin1 (); parse_rec rem
@@ -341,6 +324,8 @@ let parse () =
 	glob_source := GlobFile f; parse_rec rem
     | ("-glob-from" | "--glob-from") :: [] ->
 	usage ()
+    | ("-no-glob" | "--no-glob") :: rem ->
+	glob_source := NoGlob; parse_rec rem
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
 	Cdglobals.externals := false; parse_rec rem
     | ("--external" | "-external") :: u :: logicalpath :: rem ->
@@ -350,7 +335,11 @@ let parse () =
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
     | ("--boot" | "-boot") :: rem ->
-	Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem
+	Cdglobals.coqlib_path := normalize_path (
+          Filename.concat
+            (Filename.dirname Sys.executable_name)
+            Filename.parent_dir_name
+        ); parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
 	Cdglobals.coqlib_path := d; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: [] ->
@@ -458,13 +447,13 @@ let gen_mult_files l =
     end
       (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
 
-let read_glob_file x =
-  try Index.read_glob x
-  with Sys_error s ->
-    eprintf "Warning: %s (links will not be available)\n" s
+let read_glob_file vfile f =
+  try Index.read_glob vfile f
+  with Sys_error s -> eprintf "Warning: %s (links will not be available)\n" s
 
 let read_glob_file_of = function
-  | Vernac_file (f,_) -> read_glob_file (Filename.chop_extension f ^ ".glob")
+  | Vernac_file (f,_) ->
+      read_glob_file (Some f) (Filename.chop_extension f ^ ".glob")
   | Latex_file _ -> ()
 
 let index_module = function
@@ -486,7 +475,7 @@ let produce_document l =
   (match !Cdglobals.glob_source with
     | NoGlob -> ()
     | DotGlob -> List.iter read_glob_file_of l
-    | GlobFile f -> read_glob_file f);
+    | GlobFile f -> read_glob_file None f);
   List.iter index_module l;
   match !out_to with
     | StdOut ->
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index eefcfd11..0dc86bc8 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Cdglobals
 open Index
 
@@ -32,24 +29,27 @@ let build_table l =
 
 let is_keyword =
   build_table
-    [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
+    [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
       "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
-      "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
+      "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar";
+      "Guarded"; "Goal"; "Hint"; "Debug"; "On";
       "Hypothesis"; "Hypotheses";
-      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
+      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite";
+      "Implicit"; "Import"; "Inductive";
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
       "Module"; "Module Type"; "Declare Module"; "Include";
-      "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed";
-      "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
+      "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
+      "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
+      "Search"; "SearchAbout"; "SearchRewrite";
       "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
-      "Delimit"; "Bind"; "Open"; "Scope";
-      "Boxed"; "Unboxed"; "Inline";
+      "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
       "Implicit Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
-      "subgoal";
-      "Opaque"; "Transparent";
+      "subgoal"; "subgoals"; "vm_compute";
+      "Opaque"; "Transparent"; "Time";
+      "Extraction"; "Extract";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -57,14 +57,20 @@ let is_keyword =
       (*i (* coq terms *) *)
       "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun";
       "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
+      "fix"; "cofix";
       (* Ltac *)
-      "before"; "after"
+      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta";
+      (* Notations *)
+      "level"; "associativity"; "no"
        ]
 
 let is_tactic =
   build_table
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
-      "elimtype"; "progress"; "setoid_rewrite";
+      "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
+      "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
+      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate";
+      "quote"; "eexact"; "autorewrite";
       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
       "set"; "assert"; "do"; "repeat";
@@ -73,8 +79,10 @@ let is_tactic =
       "reflexivity"; "symmetry"; "transitivity";
       "replace"; "setoid_replace"; "inversion"; "inversion_clear";
       "pattern"; "intuition"; "congruence"; "fail"; "fresh";
-      "trivial"; "exact"; "tauto"; "firstorder"; "ring";
-      "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ]
+      "trivial"; "tauto"; "firstorder"; "ring";
+      "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto";
+      "change"; "fold"; "hnf"; "lazy"; "simple"; "eexists"; "debug"; "idtac"; "first"; "type of"; "pose";
+      "eval"; "instantiate"; "until" ]
 
 (*s Current Coq module *)
 
@@ -118,9 +126,12 @@ let initialize_texmacs () =
 
 let token_tree_texmacs = ref (initialize_texmacs ())
 
+let token_tree_latex = ref Tokens.empty_ttree
+let token_tree_html = ref Tokens.empty_ttree
+
 let initialize_tex_html () =
   let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
-    List.fold_right (fun (s,l,l') (tt,tt') ->
+  let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') ->
       (Tokens.ttree_add tt s l,
        match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l'))
       [ "*" ,  "\\ensuremath{\\times}", if_utf8 "×";
@@ -143,10 +154,9 @@ let initialize_tex_html () =
 	"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
 	"λ", "\\ensuremath{\\lambda}", if_utf8 "λ";
 	(* "fun", "\\ensuremath{\\lambda}" ? *)
-      ] (Tokens.empty_ttree,Tokens.empty_ttree)
-
-let token_tree_latex = ref (fst (initialize_tex_html ()))
-let token_tree_html = ref (snd (initialize_tex_html ()))
+      ] (Tokens.empty_ttree,Tokens.empty_ttree) in
+  token_tree_latex := tree_latex;
+  token_tree_html  := tree_html
 
 let add_printing_token s (t1,t2) =
   (match t1 with None -> () | Some t1 ->
@@ -182,10 +192,20 @@ module Latex = struct
 
   let push_in_preamble s = Queue.add s preamble
 
+  let utf8x_extra_support () =
+    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 "\\usepackage{tipa}\n";
+    printf "\n"
+
   let header () =
     if !header_trailer then begin
       printf "\\documentclass[12pt]{report}\n";
       if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc;
+      if !inputenc = "utf8x" then utf8x_extra_support ();
       printf "\\usepackage[T1]{fontenc}\n";
       printf "\\usepackage{fullpage}\n";
       printf "\\usepackage{coqdoc}\n";
@@ -255,6 +275,12 @@ module Latex = struct
 	| '^' | '~' as c ->
 	    Buffer.add_char buff '\\'; Buffer.add_char buff c;
 	    Buffer.add_string buff "{}"
+        | '\'' ->
+            if i < String.length s - 1 && s.[i+1] = '\'' then begin
+              Buffer.add_char buff '\''; Buffer.add_char buff '{';
+              Buffer.add_char buff '}'
+            end else
+              Buffer.add_char buff '\''
 	| c ->
 	    Buffer.add_char buff c
       done;
@@ -276,9 +302,23 @@ module Latex = struct
 
   let stop_latex_math () = output_char '$'
 
-  let start_verbatim () = printf "\\begin{verbatim}"
+  let start_quote () = output_char '`'; output_char '`'
+  let stop_quote () = output_char '\''; output_char '\''
+    
+  let start_verbatim inline = 
+    if inline then printf "\\texttt{"
+    else printf "\\begin{verbatim}"
 
-  let stop_verbatim () = printf "\\end{verbatim}\n"
+  let stop_verbatim inline =
+    if inline then printf "}"
+    else printf "\\end{verbatim}\n"
+
+  let url addr name = 
+    printf "%s\\footnote{\\url{%s}}"
+      (match name with
+       | None -> ""
+       | Some n -> n)
+      addr
 
   let indentation n =
     if n == 0 then
@@ -287,9 +327,6 @@ module Latex = struct
       let space = 0.5 *. (float n) in
       printf "\\coqdocindent{%2.2fem}\n" space
 
-  let module_ref m s =
-    printf "\\coqdocmodule{%s}{%s}" m (escaped s)
-
   let ident_ref m fid typ s =
     let id = if fid <> "" then (m ^ "." ^ fid) else m in
     match find_module m with
@@ -306,18 +343,20 @@ module Latex = struct
 	  printf "\\coqdoc%s{%s}" (type_name typ) s
 
   let defref m id ty s =
-    printf "\\coqdef{"; label_ident (m ^ "." ^ id);
-    printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s
+    if ty <> Notation then
+      (printf "\\coqdef{"; label_ident (m ^ "." ^ id);
+       printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s)
+    else
+      (* Glob file still not able to say the exact extent of the definition *)
+      (* so we currently renounce to highlight the notation location *)
+      (printf "\\coqdef{"; label_ident (m ^ "." ^ id);
+       printf "}{%s}{%s}" s s)
 
   let reference s = function
     | Def (fullid,typ) ->
 	defref (get_module false) fullid typ s
-    | Mod (m,s') when s = s' ->
-	module_ref m s
     | Ref (m,fullid,typ) ->
 	ident_ref m fullid typ s
-    | Mod _ ->
-	printf "\\coqdocvar{%s}" (escaped s)
 
   (*s The sublexer buffers symbol characters and attached
        uninterpreted ident and try to apply special translation such as,
@@ -330,13 +369,22 @@ module Latex = struct
     | Some ref -> reference s ref
     | None -> if issymbchar then output_string s else printf "\\coqdocvar{%s}" s
 
+  let last_was_in = ref false
+
   let sublexer c loc =
-    let tag =
-      try Some (Index.find (get_module false) loc) with Not_found -> None
-    in
-    Tokens.output_tagged_symbol_char tag c
+    if c = '*' && !last_was_in then begin
+      Tokens.flush_sublexer ();
+      output_char '*'
+    end else begin
+      let tag =
+        try Some (Index.find (get_module false) loc) with Not_found -> None
+      in
+      Tokens.output_tagged_symbol_char tag c
+    end;
+    last_was_in := false
 
   let initialize () =
+    initialize_tex_html ();
     Tokens.token_tree := token_tree_latex;
     Tokens.outfun := output_sublexer_string
 
@@ -345,7 +393,11 @@ module Latex = struct
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
+  let keyword s loc = 
+    printf "\\coqdockw{%s}" (translate s)
+
   let ident s loc =
+    last_was_in := s = "in";
     try
       let tag = Index.find (get_module false) loc in
       reference (translate s) tag
@@ -478,8 +530,7 @@ module Html = struct
 	end
 
   let trailer () =
-    if !header_trailer then
-      if !footer_file_spec then
+    if !header_trailer && !footer_file_spec then
 	let cin = Pervasives.open_in !footer_file in
 	  try
 	    while true do
@@ -487,14 +538,14 @@ module Html = struct
 		printf "%s\n" s
 	    done
 	  with End_of_file -> Pervasives.close_in cin
-      else
-	begin
-	  if !index && (get_module false) <> "Index" then
-	    printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
-	  printf "<hr/>This page has been generated by ";
-	  printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
-	  printf "</div>\n\n</div>\n\n</body>\n</html>"
-	end
+    else
+      begin
+        if !index && (get_module false) <> "Index" then
+          printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
+	printf "<hr/>This page has been generated by ";
+	printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
+	printf "</div>\n\n</div>\n\n</body>\n</html>"
+      end
 
   let start_module () =
     let ln = !lib_name in
@@ -547,17 +598,22 @@ module Html = struct
   let start_latex_math () = ()
   let stop_latex_math () = ()
 
-  let start_verbatim () = printf "<pre>"
-  let stop_verbatim () = printf "</pre>\n"
+  let start_quote () = char '"'
+  let stop_quote () = start_quote ()
 
-  let module_ref m s =
-    match find_module m with
-      | Local ->
-	  printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
-      | External m when !externals ->
-	  printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
-      | External _ | Unknown ->
-	  output_string s
+  let start_verbatim inline = 
+    if inline then printf "<tt>"
+    else printf "<pre>"
+
+  let stop_verbatim inline = 
+    if inline then printf "</tt>" 
+    else printf "</pre>\n"
+
+  let url addr name = 
+    printf "<a href=\"%s\">%s</a>" addr 
+      (match name with
+       | Some n -> n
+       | None -> addr)
 
   let ident_ref m fid typ s =
     match find_module m with
@@ -575,12 +631,8 @@ module Html = struct
     | Def (fullid,ty) ->
 	printf "<a name=\"%s\">" fullid;
 	printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s
-    | Mod (m,s') when s = s' ->
-	module_ref m s
     | Ref (m,fullid,ty) ->
 	ident_ref m fullid (type_name ty) s
-    | Mod _ ->
-	printf "<span class=\"id\" type=\"mod\">%s</span>" s
 
   let output_sublexer_string doescape issymbchar tag s =
     let s = if doescape then escaped s else s in
@@ -597,12 +649,16 @@ module Html = struct
     Tokens.output_tagged_symbol_char tag c
 
   let initialize () =
+    initialize_tex_html();
     Tokens.token_tree := token_tree_html;
     Tokens.outfun := output_sublexer_string
 
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
+  let keyword s loc = 
+    printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+
   let ident s loc =
     if is_keyword s then begin
       printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
@@ -624,7 +680,7 @@ module Html = struct
 
   let rec reach_item_level n =
     if !item_level < n then begin
-      printf "<ul>\n<li>"; incr item_level;
+      printf "<ul class=\"doclist\">\n<li>"; incr item_level;
       reach_item_level n
     end else if !item_level > n then begin
       printf "\n</li>\n</ul>\n"; decr item_level;
@@ -662,7 +718,9 @@ module Html = struct
 
   let end_code () = end_coq (); start_doc ()
 
-  let start_inline_coq () = printf "<span class=\"inlinecode\">"
+  let start_inline_coq () = 
+    if !inline_notmono then printf "<span class=\"inlinecodenm\">"
+                       else printf "<span class=\"inlinecode\">"
 
   let end_inline_coq () = printf "</span>"
 
@@ -670,7 +728,50 @@ module Html = struct
 
   let end_inline_coq_block () = end_inline_coq ()
 
-  let paragraph () = printf "\n<br/> <br/>\n"
+  let paragraph () = printf "\n<div class=\"paragraph\"> </div>\n\n" 
+
+  (* inference rules *)
+  let inf_rule assumptions (_,_,midnm) conclusions =
+    (* this first function replaces any occurance of 3 or more spaces
+       in a row with "&nbsp;"s.  We do this to the assumptions so that
+       people can put multiple rules on a line with nice formatting *)
+    let replace_spaces str =
+      let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in 
+      let results = Str.full_split (Str.regexp "[' '][' '][' ']+") str in
+      let strs = List.map (fun r -> match r with
+                                    | Str.Text s  -> [s]
+                                    | Str.Delim s -> 
+                                        copy "&nbsp;" (String.length s))  
+                          results
+      in
+        String.concat "" (List.concat strs)
+    in
+    let start_assumption line =
+          (printf "<tr class=\"infruleassumption\">\n";
+           printf "  <td class=\"infrule\">%s</td>\n" (replace_spaces line)) in
+    let end_assumption () =
+          (printf "  <td></td>\n";
+           printf "</td>\n") in
+    let rec print_assumptions hyps = 
+          match hyps with
+          | []                 -> start_assumption "&nbsp;&nbsp;"
+          | [(_,hyp)]          -> start_assumption hyp
+          | ((_,hyp) :: hyps') -> (start_assumption hyp;
+                                   end_assumption ();
+                                   print_assumptions hyps') in
+    printf "<center><table class=\"infrule\">\n";
+    print_assumptions assumptions;
+    printf "  <td class=\"infrulenamecol\" rowspan=\"3\">\n";
+    (match midnm with
+     | None   -> printf "    &nbsp;\n  </td>" 
+     | Some s -> printf "    %s &nbsp;\n  </td>" s);
+    printf "</tr>\n";
+    printf "<tr class=\"infrulemiddle\">\n";
+    printf "  <td class=\"infrule\"><hr /></td>\n";
+    printf "</tr>\n";
+    print_assumptions conclusions;
+    end_assumption ();
+    printf "</table></center>"
 
   let section lev f =
     let lab = new_label () in
@@ -858,19 +959,28 @@ module TeXmacs = struct
 
   let stop_latex_math () = output_char '>'
 
-  let start_verbatim () = in_doc := true; printf "<\\verbatim>"
+  let start_verbatim inline = in_doc := true; printf "<\\verbatim>"
+  let stop_verbatim inline = in_doc := false; printf "</verbatim>"
+
+  let url addr name = 
+    printf "%s<\\footnote><\\url>%s</url></footnote>" addr
+      (match name with
+       | None -> ""
+       | Some n -> n)
 
-  let stop_verbatim () = in_doc := false; printf "</verbatim>"
+  let start_quote () = output_char '`'; output_char '`'
+  let stop_quote () = output_char '\''; output_char '\''
 
   let indentation n = ()
 
+  let keyword s =
+    printf "<kw|"; raw_ident s; printf ">"
+
   let ident_true s =
-    if is_keyword s then begin
-      printf "<kw|"; raw_ident s; printf ">"
-    end else begin
-      raw_ident s
-    end
+    if is_keyword s then keyword s
+    else raw_ident s
 
+  let keyword s loc = keyword s
   let ident s _ = if !in_doc then ident_true s else raw_ident s
 
   let output_sublexer_string doescape issymbchar tag s =
@@ -985,13 +1095,21 @@ module Raw = struct
   let start_latex_math () = ()
   let stop_latex_math () = ()
 
-  let start_verbatim () = ()
+  let start_verbatim inline = ()
+  let stop_verbatim inline = ()
 
-  let stop_verbatim () = ()
+  let url addr name = 
+    match name with
+    | Some n -> printf "%s (%s)" n addr
+    | None -> printf "%s" addr
+
+  let start_quote () = printf "\""
+  let stop_quote () = printf "\""
 
   let indentation n =
       for i = 1 to n do printf " " done
 
+  let keyword s loc = raw_ident s
   let ident s loc = raw_ident s
 
   let sublexer c l = char c
@@ -1105,6 +1223,7 @@ let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
 
 let nbsp = select Latex.nbsp Html.nbsp TeXmacs.nbsp Raw.nbsp
 let char = select Latex.char Html.char TeXmacs.char Raw.char
+let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword
 let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
 let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer
 let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize
@@ -1132,10 +1251,33 @@ let start_verbatim =
   select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim
 let stop_verbatim =
   select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
-let verbatim_char =
-  select output_char Html.char TeXmacs.char Raw.char
+let verbatim_char inline =
+  select (if inline then Latex.char else output_char) Html.char TeXmacs.char Raw.char
 let hard_verbatim_char = output_char
 
+let url = 
+  select Latex.url Html.url TeXmacs.url Raw.url
+
+let start_quote =
+  select Latex.start_quote Html.start_quote TeXmacs.start_quote Raw.start_quote
+let stop_quote =
+  select Latex.stop_quote Html.stop_quote TeXmacs.stop_quote Raw.stop_quote
+
+let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = 
+  start_verbatim false;
+  let dumb_line = 
+       function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln);
+                            char '\n')
+  in 
+    (List.iter dumb_line assumptions;
+     dumb_line (midsp, midln ^ (match midnm with 
+                                | Some s -> " " ^ s 
+                                | None -> ""));
+     List.iter dumb_line conclusions);
+  stop_verbatim false
+
+let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb
+
 let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index
 let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index
 let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index dcd9072d..80f39011 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Cdglobals
 open Index
 
@@ -62,6 +60,7 @@ val rule : unit -> unit
 
 val nbsp : unit -> unit
 val char : char -> unit
+val keyword : string -> loc -> unit
 val ident : string -> loc -> unit
 val sublexer : char -> loc -> unit
 val initialize : unit -> unit
@@ -72,13 +71,34 @@ val latex_char : char -> unit
 val latex_string : string -> unit
 val html_char : char -> unit
 val html_string : string -> unit
-val verbatim_char : char -> unit
+val verbatim_char : bool -> char -> unit
 val hard_verbatim_char : char -> unit
 
 val start_latex_math : unit -> unit
 val stop_latex_math : unit -> unit
-val start_verbatim : unit -> unit
-val stop_verbatim : unit -> unit
+val start_verbatim : bool -> unit
+val stop_verbatim : bool -> unit
+val start_quote : unit -> unit
+val stop_quote : unit -> unit
+
+val url : string -> string option -> unit
+
+(* this outputs an inference rule in one go.  You pass it the list of
+   assumptions, then the middle line info, then the conclusion (which
+   is allowed to span multiple lines).
+
+   In each case, the int is the number of spaces before the start of
+   the line's text and the string is the text of the line with the
+   leading trailing space trimmed.  For the middle rule, you can
+   also optionally provide a name.
+
+   We need the space info so that in modes where we aren't doing
+   something smart we can just format the rule verbatim like the user did
+*)
+val inf_rule :  (int * string) list
+             -> (int * string * (string option)) 
+             -> (int * string) list
+             -> unit
 
 val make_multi_index : unit -> unit
 val make_index : unit -> unit
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index 9de39083..10a105f9 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-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \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 3b756e18..e9c74307 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-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)