Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

7 files changed, 764 insertions, 436 deletions

diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 8a774876..44b9bd3c 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -26,14 +26,18 @@ let out_to = ref MultFiles
 let out_channel = ref stdout
 
 let open_out_file f =
-  let f = if !output_dir <> "" then Filename.concat !output_dir f else f in
+  let f = if !output_dir <> "" && Filename.is_relative f then Filename.concat !output_dir f else f in
     out_channel := open_out f
 
 let close_out_file () = close_out !out_channel
 
 
 let header_trailer = ref true
-let quiet = ref false
+let header_file = ref ""
+let header_file_spec = ref false
+let footer_file = ref ""
+let footer_file_spec = ref false
+let quiet = ref true
 let light = ref false
 let gallina = ref false
 let short = ref false
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index 2c07b9fc..d31314c5 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -8,20 +8,20 @@
 \NeedsTeXFormat{LaTeX2e}
 \ProvidesPackage{coqdoc}[2002/02/11]
 
-% Headings
-\usepackage{fancyhdr}
-\newcommand{\coqdocleftpageheader}{\thepage\ -- \today}
-\newcommand{\coqdocrightpageheader}{\today\ -- \thepage}
-\pagestyle{fancyplain}
+% % Headings
+% \usepackage{fancyhdr}
+% \newcommand{\coqdocleftpageheader}{\thepage\ -- \today}
+% \newcommand{\coqdocrightpageheader}{\today\ -- \thepage}
+% \pagestyle{fancyplain}
 
-%BEGIN LATEX
-\headsep 8mm
-\renewcommand{\plainheadrulewidth}{0.4pt}
-\renewcommand{\plainfootrulewidth}{0pt}
-\lhead[\coqdocleftpageheader]{\leftmark}
-\rhead[\leftmark]{\coqdocrightpageheader}
-\cfoot{}
-%END LATEX
+% %BEGIN LATEX
+% \headsep 8mm
+% \renewcommand{\plainheadrulewidth}{0.4pt}
+% \renewcommand{\plainfootrulewidth}{0pt}
+% \lhead[\coqdocleftpageheader]{\leftmark}
+% \rhead[\leftmark]{\coqdocrightpageheader}
+% \cfoot{}
+% %END LATEX
 
 % Hevea puts to much space with \medskip and \bigskip
 %HEVEA\renewcommand{\medskip}{}
@@ -36,11 +36,27 @@
 %END LATEX
 
 % macro for typesetting keywords
-\newcommand{\coqdockw}[1]{\textsf{#1}}
+\newcommand{\coqdockw}[1]{\texttt{#1}}
 
-% macro for typesetting identifiers
+% macro for typesetting variable identifiers
 \newcommand{\coqdocid}[1]{\textit{#1}}
 
+% macro for typesetting constant identifiers
+\newcommand{\coqdoccst}[1]{\textsf{#1}}
+
+% macro for typesetting module identifiers
+\newcommand{\coqdocmod}[1]{\textsc{\textsf{#1}}}
+
+% macro for typesetting module constant identifiers (e.g. Parameters in
+% module types)
+\newcommand{\coqdocax}[1]{\textsl{\textsf{#1}}}
+
+% macro for typesetting inductive type identifiers
+\newcommand{\coqdocind}[1]{\textbf{\textsf{#1}}}
+
+% macro for typesetting constructor identifiers
+\newcommand{\coqdocconstr}[1]{\textsf{#1}}
+
 % newline and indentation 
 %BEGIN LATEX
 \newcommand{\coqdoceol}{\setlength\parskip{0pt}\par}
@@ -52,6 +68,86 @@
 % macro for typesetting the title of a module implementation
 \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
 }
+\usepackage{ifpdf}
+\ifpdf
+  \usepackage[pdftex]{hyperref}
+  \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black}
+  \usepackage[all]{hypcap}
+
+  \newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}}
+  \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
+  \newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}
+  \newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection
+    \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}}
+\else
+  \newcommand{\coqdef}[3]{#3}
+  \newcommand{\coqref}[2]{#2}
+  \newcommand{\identref}[2]{\textsf {#2}}
+  \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}}
+\fi
+\usepackage{xr}
+
+%\usepackage{color}
+%\usepackage{multind}
+%\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
+
+  
+
+\newcommand{\coqdocvar}[1]{{\textit{#1}}}
+\newcommand{\coqdoctac}[1]{{\texttt{#1}}}
+
+
+\newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+%\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
+%\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
+\newcommand{\coqvariable}[2]{\coqdocid{#2}}
+
+\newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
+\newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}}
+
+\newcommand{\coqconstructor}[2]{\coqdef{#1}{#2}{\coqdocconstr{#2}}}
+\newcommand{\coqconstructorref}[2]{\coqref{#1}{\coqdocconstr{#2}}}
+
+\newcommand{\coqlemma}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqlemmaref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqclass}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
+\newcommand{\coqclassref}[2]{\coqref{#1}{\coqdocind{#2}}}
+
+\newcommand{\coqinstance}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqinstanceref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqmethod}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqmethodref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqabbreviation}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqabbreviationref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqrecord}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
+\newcommand{\coqrecordref}[2]{\coqref{#1}{\coqdocind{#2}}}
+
+\newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}}
+
+\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+%\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}}
+  
+%\newcommand{\coqlibraryref}[2]{\ref{coq:#1}}
+
+\newcommand{\coqlibraryref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}}
+\newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}}
+
+\newcommand{\coqmodule}[2]{\coqdef{#1}{#2}{\coqdocmod{#2}}}
+\newcommand{\coqmoduleref}[2]{\coqref{#1}{\coqdocmod{#2}}}
+
 
 %HEVEA\newcommand{\lnot}{\coqwkw{not}}
 %HEVEA\newcommand{\lor}{\coqwkw{or}}
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 4b53d6ff..1da8ebd7 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mli 8617 2006-03-08 10:47:12Z notin $ i*)
+(*i $Id: index.mli 11065 2008-06-06 22:39:43Z msozeau $ i*)
 
 open Cdglobals
 
@@ -19,13 +19,23 @@ type entry_type =
   | Inductive
   | Constructor
   | Lemma
+  | Record
+  | Projection
+  | Instance
+  | Class
+  | Method
   | Variable
   | Axiom
   | TacticDefinition
+  | Abbreviation
+  | Notation
+  | Section
+
+val type_name : entry_type -> string
 
 type index_entry = 
   | Def of string * entry_type
-  | Ref of coq_module * string
+  | Ref of coq_module * string * entry_type
   | Mod of coq_module * string
 
 val find : coq_module -> loc -> index_entry
@@ -42,7 +52,7 @@ val scan_file : string -> coq_module -> unit
 
 (*s Read globalizations from a file (produced by coqc -dump-glob) *)
 
-val read_glob : string -> unit
+val read_glob : string -> coq_module
 
 (*s Indexes *)
 
@@ -51,6 +61,8 @@ type 'a index = {
   idx_entries : (char * (string * 'a) list) list;
   idx_size : int }
 
+val current_library : string ref
+
 val all_entries : unit -> 
       (coq_module * entry_type) index *
       (entry_type * coq_module index) list
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 5b281b8b..fc2090dc 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mll 9204 2006-10-04 13:05:58Z notin $ i*)
+(*i $Id: index.mll 11065 2008-06-06 22:39:43Z msozeau $ i*)
 
 {
 
@@ -25,31 +26,49 @@ type entry_type =
   | Inductive
   | Constructor
   | Lemma
+  | Record
+  | Projection
+  | Instance
+  | Class
+  | Method
   | Variable
   | Axiom
   | TacticDefinition
+  | Abbreviation
+  | Notation
+  | Section
 
 type index_entry = 
   | Def of string * entry_type
-  | Ref of coq_module * string
+  | Ref of coq_module * string * entry_type
   | Mod of coq_module * string
 
 let current_type = ref Library
 let current_library = ref ""
-  (** referes to the file being parsed *)
+  (** refers to the file being parsed *)
 
 let table = Hashtbl.create 97
   (** [table] is used to store references and definitions *)
 
-let add_def loc ty id = Hashtbl.add table (!current_library, loc) (Def (id, ty))
-
-let add_ref m loc m' id = Hashtbl.add table (m, loc) (Ref (m', id))
+let full_ident sp id =
+  if sp <> "<>" then 
+    if id <> "<>" then 
+      sp ^ "." ^ id 
+    else sp 
+  else if id <> "<>" 
+  then id 
+  else ""
+    
+let add_def loc ty sp id = 
+  Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty))
 
+let add_ref m loc m' sp id ty = 
+  Hashtbl.add table (m, loc) (Ref (m', full_ident sp id, ty))
+    
 let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
 
 let find m l = Hashtbl.find table (m, l)
 
-
 (*s Manipulating path prefixes *) 
 
 type stack = string list 
@@ -99,14 +118,15 @@ let make_fullid id =
     else 
       id
 
+
 (* Coq modules *)
 
 let split_sp s = 
   try
     let i = String.rindex s '.' in
-    String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
-  with Not_found -> 
-    "", s
+      String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
+  with 
+      Not_found -> "", s
 
 let modules = Hashtbl.create 97
 let local_modules = Hashtbl.create 97
@@ -118,8 +138,7 @@ let add_module m =
 
 type module_kind = Local | Coqlib | Unknown
 
-let coq_module m =
-  String.length m >= 4 && String.sub m 0 4 = "Coq."
+let coq_module m = String.length m >= 4 && String.sub m 0 4 = "Coq."
 
 let find_module m =
   if Hashtbl.mem local_modules m then 
@@ -129,14 +148,6 @@ let find_module m =
   else
     Unknown
 
-let ref_module loc s =
-  try
-    let n = String.length s in
-    let i = String.rindex s ' ' in 
-    let id = String.sub s (i+1) (n-i-1) in
-      add_mod !current_library (loc+i+1) (Hashtbl.find modules id) id
-  with Not_found -> 
-    ()
 
 (* Building indexes *)
 
@@ -181,10 +192,18 @@ let type_name = function
   | Inductive -> "inductive"
   | Constructor -> "constructor"
   | Lemma -> "lemma"
+  | Record -> "record"
+  | Projection -> "projection"
+  | Instance -> "instance"
+  | Class -> "class"
+  | Method -> "method"
   | Variable -> "variable"
   | Axiom -> "axiom"
   | TacticDefinition -> "tactic"
-      
+  | Abbreviation -> "abbreviation"
+  | Notation -> "notation"
+  | Section -> "section"
+
 let all_entries () =
   let gl = ref [] in
   let add_g s m t = gl := (s,(m,t)) :: !gl in
@@ -209,6 +228,8 @@ let all_entries () =
 }
 
 (*s Shortcuts for regular expressions. *)
+let digit = ['0'-'9']
+let num = digit+
 
 let space = 
   [' ' '\010' '\013' '\009' '\012']
@@ -225,16 +246,18 @@ let end_hide = "(*" space* "end" space+ "hide" space* "*)"
 (*s Indexing entry point. *)
   
 rule traverse = parse
-  | "Definition" space
+  | ("Program" space+)? "Definition" space
       { current_type := Definition; index_ident lexbuf; traverse lexbuf }
   | "Tactic" space+ "Definition" space
       { current_type := TacticDefinition; index_ident lexbuf; traverse lexbuf }
   | ("Axiom" | "Parameter") space 
       { current_type := Axiom; index_ident lexbuf; traverse lexbuf }
-  | "Fixpoint" space
+  | ("Program" space+)? "Fixpoint" space
       { current_type := Definition; index_ident lexbuf; fixpoint lexbuf;
 	traverse lexbuf }
-  | ("Lemma" | "Theorem") space
+  | ("Program" space+)? ("Lemma" | "Theorem") space
+      { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
+  | "Obligation" space num ("of" ident)?
       { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
   | "Inductive" space
       { current_type := Inductive; 
@@ -247,8 +270,8 @@ rule traverse = parse
   | "Variable" 's'? space
       { current_type := Variable; index_idents lexbuf; traverse lexbuf }
 ***i*)
-  | "Require" (space+ ("Export"|"Import"))? space+ ident
-      { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf }
+  | "Require" (space+ ("Export"|"Import"))? 
+      { module_refs lexbuf; traverse lexbuf }
   | "End" space+ 
       { end_ident lexbuf; traverse lexbuf }
   | begin_hide 
@@ -277,7 +300,7 @@ and index_ident = parse
 	      | Lemma -> make_fullid id
 	      | _ -> id 
 	in 
-	  add_def (lexeme_start lexbuf) !current_type fullid }
+	  add_def (lexeme_start lexbuf) !current_type "" fullid }
   | eof    
       { () }
   | _      
@@ -289,7 +312,7 @@ and index_idents = parse
   | space+ | ','
       { index_idents lexbuf }
   | ident  
-      { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf);
+      { add_def (lexeme_start lexbuf) !current_type "" (lexeme lexbuf);
 	index_idents lexbuf }
   | eof    
       { () }
@@ -369,14 +392,52 @@ and module_ident = parse
       { () }
   | ident
       { let id = lexeme lexbuf in
-	  begin_module id; add_def (lexeme_start lexbuf) !current_type id }
+	  begin_module id; add_def (lexeme_start lexbuf) !current_type "" id }
   | eof
       { () }
   | _
       { () }
 
+(*s parse module names *)
+
+and module_refs = parse
+  | space+ 
+      { module_refs lexbuf }
+  | ident  
+      { let id =  lexeme lexbuf in
+	  (try
+	      add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
+	    with
+		Not_found -> ()
+	  ); 
+	module_refs lexbuf }
+  | eof    
+      { () }
+  | _      
+      { () }
+
 {
-  
+  let type_of_string = function
+    | "def" | "coe" | "subclass" | "canonstruc" 
+    | "ex" | "scheme" -> Definition
+    | "prf" | "thm" -> Lemma
+    | "ind" | "coind" -> Inductive
+    | "constr" -> Constructor
+    | "rec" | "corec" -> Record
+    | "proj" -> Projection
+    | "class" -> Class
+    | "meth" -> Method
+    | "inst" -> Instance
+    | "var" -> Variable
+    | "defax" | "prfax" | "ax" -> Axiom
+    | "syndef" -> Abbreviation
+    | "not" -> Notation
+    | "lib" -> Library
+    | "mod" | "modtype" -> Module
+    | "tac" -> TacticDefinition
+    | "sec" -> Section
+    | s -> raise (Invalid_argument ("type_of_string:" ^ s))
+	
   let read_glob f = 
     let c = open_in f in
     let cur_mod = ref "" in
@@ -387,22 +448,22 @@ and module_ident = parse
 	if n > 0 then begin
 	  match s.[0] with
 	    | 'F' -> 
-		cur_mod := String.sub s 1 (n - 1)
+		cur_mod := String.sub s 1 (n - 1);
+		current_library := !cur_mod
 	    | 'R' ->
 		(try
-		   let i = String.index s ' ' in
-		   let j = String.index_from s (i+1) ' ' in 
-		   let loc = int_of_string (String.sub s 1 (i - 1)) in
-		   let lib_dp = String.sub s (i + 1) (j - i - 1) in
-		   let full_id = String.sub s (j + 1) (n - j - 1) in
-		     add_ref !cur_mod loc lib_dp full_id
-		 with Not_found -> 
-		   ())
-	    | _ -> ()
+		    Scanf.sscanf s "R%d %s %s %s %s"
+		      (fun loc lib_dp sp id ty ->
+			add_ref !cur_mod loc lib_dp sp id (type_of_string ty))
+		  with _ -> ())
+	    | _ -> 
+		try Scanf.sscanf s "%s %d %s %s"
+		  (fun ty loc sp id -> add_def loc (type_of_string ty) sp id)
+		with Scanf.Scan_failure _ -> ()
 	end
-      done
+      done; assert false
     with End_of_file -> 
-      close_in c
+      close_in c; !cur_mod
 	
   let scan_file f m = 
     init_stack (); current_library := m;
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 18a44a44..7111187f 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 8777 2006-05-02 10:14:39Z notin $ i*)
+(*i $Id: main.ml 11024 2008-05-30 12:41:39Z msozeau $ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -19,50 +20,53 @@
  *)
 
 open Cdglobals
-open Filename
 open Printf
-open Output
-open Pretty
 
 (*s \textbf{Usage.} Printed on error output. *)
 
 let usage () =
   prerr_endline "";
   prerr_endline "Usage: coqdoc <options and files>";
-  prerr_endline "  --html              produce a HTML document (default)";
-  prerr_endline "  --latex             produce a LaTeX document";
-  prerr_endline "  --texmacs           produce a TeXmacs document";
-  prerr_endline "  --dvi               output the DVI";
-  prerr_endline "  --ps                output the PostScript";
-  prerr_endline "  --stdout            write output to stdout";
-  prerr_endline "  -o <file>           write output in file <file>";
-  prerr_endline "  -d <dir>            output files into directory <dir>";
-  prerr_endline "  -g                  (gallina) skip proofs";
-  prerr_endline "  -s                  (short) no titles for files";
-  prerr_endline "  -l                  light mode (only defs and statements)";
-  prerr_endline "  -t <string>         give a title to the document";
-  prerr_endline "  --body-only         suppress LaTeX/HTML header and trailer";
-  prerr_endline "  --no-index          do not output the index";
-  prerr_endline "  --multi-index       index split in multiple files";
-  prerr_endline "  --toc               output a table of contents";
-  prerr_endline "  --vernac <file>     consider <file> as a .v file";
-  prerr_endline "  --tex <file>        consider <file> as a .tex file";
-  prerr_endline "  -p <string>         insert <string> in LaTeX preamble";
-  prerr_endline "  --files-from <file> read file names to process in <file>";
-  prerr_endline "  --quiet             quiet mode";
-  prerr_endline "  --glob-from <file>  read Coq globalizations from file <file>";
-  prerr_endline "  --no-externals      no links to Coq standard library";
-  prerr_endline "  --coqlib <url>      set URL for Coq standard library";
-  prerr_endline "                      (default is http://coq.inria.fr/library/)";
-  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 "  --latin1            set ISO-8859-1 input language";
-  prerr_endline "  --utf8              set UTF-8 input language";
-  prerr_endline "  --charset <string>  set HTML charset";
-  prerr_endline "  --inputenc <string> set LaTeX input encoding";
+  prerr_endline "  --html               produce a HTML document (default)";
+  prerr_endline "  --latex              produce a LaTeX document";
+  prerr_endline "  --texmacs            produce a TeXmacs document";
+  prerr_endline "  --dvi                output the DVI";
+  prerr_endline "  --ps                 output the PostScript";
+  prerr_endline "  --pdf                output the Pdf";
+  prerr_endline "  --stdout             write output to stdout";
+  prerr_endline "  -o <file>            write output in file <file>";
+  prerr_endline "  -d <dir>             output files into directory <dir>";
+  prerr_endline "  -g                   (gallina) skip proofs";
+  prerr_endline "  -s                   (short) no titles for files";
+  prerr_endline "  -l                   light mode (only defs and statements)";
+  prerr_endline "  -t <string>          give a title to the document";
+  prerr_endline "  --body-only          suppress LaTeX/HTML header and trailer";
+  prerr_endline "  --with-header <file> prepend <file> as html reader";
+  prerr_endline "  --with-footer <file> append <file> as html footer";
+  prerr_endline "  --no-index           do not output the index";
+  prerr_endline "  --multi-index        index split in multiple files";
+  prerr_endline "  --toc                output a table of contents";
+  prerr_endline "  --vernac <file>      consider <file> as a .v file";
+  prerr_endline "  --tex <file>         consider <file> as a .tex file";
+  prerr_endline "  -p <string>          insert <string> in LaTeX preamble";
+  prerr_endline "  --files-from <file>  read file names to process in <file>";
+  prerr_endline "  --quiet              quiet mode (default)";
+  prerr_endline "  --verbose            verbose mode";  
+  prerr_endline "  --no-externals       no links to Coq standard library";
+  prerr_endline "  --coqlib <url>       set URL for Coq standard library";
+  prerr_endline "                       (default is http://coq.inria.fr/library/)";
+  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 "  --latin1             set ISO-8859-1 input language";
+  prerr_endline "  --utf8               set UTF-8 input language";
+  prerr_endline "  --charset <string>   set HTML charset";
+  prerr_endline "  --inputenc <string>  set LaTeX input encoding";
   prerr_endline "";
   exit 1
 
+let obsolete s =
+  eprintf "Warning: option %s is now obsolete; please update your scripts\n" s
+
 (*s \textbf{Banner.} Always printed. Notice that it is printed on error
     output, so that when the output of [coqdoc] is redirected this header
     is not (unless both standard and error outputs are redirected, of 
@@ -74,7 +78,7 @@ let banner () =
   flush stderr
     
 let target_full_name f = 
-  match !target_language with
+  match !Cdglobals.target_language with
     | HTML -> f ^ ".html"
     | _ -> f ^ ".tex"
 	
@@ -88,95 +92,70 @@ let check_if_file_exists f =
     eprintf "\ncoqdoc: %s: no such file\n" f;
     exit 1
   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
+    Filename.concat (normalize_path dirname) basename
+
+(* [paths] maps a physical path to a name *)
 let paths = ref []
   
-let add_path m l = paths := (m,l) :: !paths
+let add_path dir name = 
+  (* if dir is relative we add both the relative and absolute name *)
+  let p = normalize_path dir in
+    paths := (p,name) :: !paths
   
-let exists_dir dir =
-  try let _ = Unix.opendir dir in true with Unix.Unix_error _ -> false
-
-let add_rec_path f l =
-  let rec traverse abs rel =
-    add_path abs rel;
-    let dirh = Unix.opendir abs in
-      try
-	while true do
-	  let f = Unix.readdir dirh in
-	    if f <> "" && f.[0] <> '.' && f <> "CVS" then
-	      let abs' = Filename.concat abs f in
-		try 
-		  if exists_dir abs' then  traverse abs' (rel ^ "." ^ f)
-		with Unix.Unix_error _ -> 
-		  ()
-	done
-      with End_of_file ->
-	Unix.closedir dirh
-  in
-    if exists_dir f then traverse f l
-
 (* turn A/B/C into A.B.C *)
-let make_path = Str.global_replace (Str.regexp "/") ".";;
+let name_of_path = Str.global_replace (Str.regexp "/") ".";;
 
-let coq_module file = 
-  (* TODO
-   * LEM:
-   * We should also remove things like "/./" in the middle of the filename,
-   * rewrite "/foo/../bar" to "/bar", recognise different paths that lead
-   * to the same file / directory (via symlinks), etc. The best way to do
-   * all this would be to use the libc function realpath() on _both_ p and
-   * file / f before comparing them.
-   *
-   * The semantics of realpath() on file symlinks might not be what we
-   * want... (But it is what we want on directory symlinks.) So, we would
-   * have to cook up our own version of realpath()?
-   *
-   * Do all target platforms have realpath()?
-   *)
-  let f = chop_extension file in
-    (* remove leading ./ and any number of slashes after *)
-  let f = Str.replace_first (Str.regexp "^\\./+") "" f in
-    if (Str.string_before f 1) = "/" then
-      (* f is an absolute path. Prefixes must be matched with the beginning of f,
-       * not prepended
-       *)
-      let rec trypath = function
-	| [] -> make_path f
-	| (p, lg) :: r ->
-            (* make sure p ends with a single '/'
-             * This guarantees that we don't match a file whose name is
-             * of the form p ^ "foo". It means we may miss p itself,
-             * but this does not matter: coqdoc doesn't do anything
-             * of a directory anyway. *)
-            let p = (Str.replace_first (Str.regexp "/*$") "/" p) in
-            let p_quoted = (Str.quote p) in
-              if (Str.string_match (Str.regexp p_quoted) f 0) then
-		make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f))
-              else
-		trypath r
-      in trypath !paths
-    else (* f is a relative path *)
-      let rec trypath = function
-	| [] -> 
-	    make_path f
-	| (p,lg) :: r ->
-	    let p_file = Filename.concat p file in
-	      if Sys.file_exists p_file then
-		make_path (Filename.concat lg f)
-	      else
-		trypath r
-      in trypath !paths;;
+let coq_module filename = 
+  let bfname = Filename.chop_extension filename in
+  let nfname = normalize_filename bfname in
+  let rec change_prefix map f = 
+    match map with
+      | [] -> 
+	  (* There is no prefix alias; 
+	     we just cut the name wrt current working directory *)
+	  let cwd = Sys.getcwd () in
+	  let exp = Str.regexp (Str.quote (cwd ^ "/")) in
+	    if (Str.string_match exp f 0) then
+	      name_of_path (Str.replace_first exp "" f)
+	    else
+	      name_of_path f
+      | (p, name) :: rem ->
+          let expp = Str.regexp (Str.quote p) in
+	    if (Str.string_match expp f 0) then
+	      let newp = Str.replace_first expp name f in
+		name_of_path newp
+            else
+	      change_prefix rem f
+  in
+    change_prefix !paths nfname
 
 let what_file f =
   check_if_file_exists f;
-  if check_suffix f ".v" || check_suffix f ".g" then
+  if Filename.check_suffix f ".v" || Filename.check_suffix f ".g" then
     Vernac_file (f, coq_module f)
-  else if check_suffix f ".tex" then
+  else if Filename.check_suffix f ".tex" then
     Latex_file f
-  else begin
-    eprintf "\ncoqdoc: don't know what to do with %s\n" f;
-    exit 1
-  end
+  else 
+     (eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1)
     
 (*s \textbf{Reading file names from a file.} 
  *  File names may be given
@@ -214,9 +193,9 @@ let files_from_file f =
       
 (*s \textbf{Parsing of the command line.} *)
       
-let output_file = ref ""
 let dvi = ref false
 let ps = ref false
+let pdf = ref false
 
 let parse () =
   let files = ref [] in
@@ -227,8 +206,16 @@ let parse () =
     | ("-nopreamble" | "--nopreamble" | "--no-preamble"
       |  "-bodyonly"   | "--bodyonly"   | "--body-only") :: rem ->
 	header_trailer := false; parse_rec rem
+    | ("-with-header" | "--with-header") :: f ::rem ->
+	header_trailer := true; header_file_spec := true; header_file := f; parse_rec rem
+    | ("-with-header" | "--with-header") :: [] ->
+	usage ()
+    | ("-with-footer" | "--with-footer") :: f ::rem ->
+	header_trailer := true; footer_file_spec := true; footer_file := f; parse_rec rem
+    | ("-with-footer" | "--with-footer") :: [] ->
+	usage ()
     | ("-p" | "--preamble") :: s :: rem ->
-	push_in_preamble s; parse_rec rem
+	Output.push_in_preamble s; parse_rec rem
     | ("-p" | "--preamble") :: [] ->
 	usage ()
     | ("-noindex" | "--noindex" | "--no-index") :: rem ->
@@ -259,6 +246,8 @@ let parse () =
 	usage ()
     | ("-latex" | "--latex") :: rem ->
 	Cdglobals.target_language := LaTeX; parse_rec rem
+    | ("-pdf" | "--pdf") :: rem ->
+	Cdglobals.target_language := LaTeX; pdf := true; parse_rec rem
     | ("-dvi" | "--dvi") :: rem ->
 	Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem
     | ("-ps" | "--ps") :: rem ->
@@ -284,10 +273,12 @@ let parse () =
 	  
     | ("-q" | "-quiet" | "--quiet") :: rem ->
 	quiet := true; parse_rec rem
+    | ("-v" | "-verbose" | "--verbose") :: rem ->
+	quiet := false; parse_rec rem
 	  
     | ("-h" | "-help" | "-?" | "--help") :: rem ->
 	banner (); usage ()
-    | ("-v" | "-version" | "--version") :: _ ->
+    | ("-V" | "-version" | "--version") :: _ ->
 	banner (); exit 0
 
     | ("-vernac-file" | "--vernac-file") :: f :: rem -> 
@@ -309,7 +300,7 @@ let parse () =
     | "-R" :: ([] | [_]) ->
 	usage ()
     | ("-glob-from" | "--glob-from") :: f :: rem ->
-	Index.read_glob f; parse_rec rem
+	obsolete "glob-from"; parse_rec rem
     | ("-glob-from" | "--glob-from") :: [] ->
 	usage ()
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
@@ -332,7 +323,7 @@ let parse () =
 (*s The following function produces the output. The default output is
     the \LaTeX\ document: in that case, we just call [Web.produce_document]. 
     If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
-    we make calls to \verb!latex! or \verb!dvips!  accordingly. *)
+    we make calls to \verb!latex! or \verb!dvips! or \verb!pdflatex! accordingly. *)
 
 let locally dir f x =
   let cwd = Sys.getcwd () in
@@ -346,8 +337,10 @@ let clean_temp_files basefile =
     remove (basefile ^ ".tex");
     remove (basefile ^ ".log");
     remove (basefile ^ ".aux");
+    remove (basefile ^ ".toc");
     remove (basefile ^ ".dvi");
     remove (basefile ^ ".ps");
+    remove (basefile ^ ".pdf");
     remove (basefile ^ ".haux");
     remove (basefile ^ ".html")
       
@@ -370,70 +363,81 @@ let copy src dst =
 
 
 (*s Functions for generating output files *)
-	
+
 let gen_one_file l =
   let file = function
     | Vernac_file (f,m) -> 
-	set_module m; coq_file f m
+	Output.set_module m; Pretty.coq_file f m
     | Latex_file _ -> ()
   in
-    if (!header_trailer) then header ();
-    if !toc then make_toc ();
+    if (!header_trailer) then Output.header ();
+    if !toc then Output.make_toc ();
     List.iter file l;
-    if !index then make_index();
-    if (!header_trailer) then trailer ()
+    if !index then Output.make_index();
+    if (!header_trailer) then Output.trailer ()
       
 let gen_mult_files l =
   let file = function
     | Vernac_file (f,m) -> 
-	set_module m;
+	Output.set_module m;
 	let hf = target_full_name m in
 	  open_out_file hf;
-	  if (!header_trailer) then header (); 
-	  if !toc then make_toc ();
-	  coq_file f m; 
-	  if (!header_trailer) then trailer ();
+	  if (!header_trailer) then Output.header (); 
+	  Pretty.coq_file f m; 
+	  if (!header_trailer) then Output.trailer ();
 	  close_out_file()
     | Latex_file _ -> ()
   in
     List.iter file l;
     if (!index && !target_language=HTML) then begin
-      if (!multi_index) then make_multi_index (); 
+      if (!multi_index) then Output.make_multi_index (); 
       open_out_file "index.html"; 
       page_title := (if !title <> "" then !title else "Index");
-      if (!header_trailer) then header (); 
-      make_index (); 
-      if (!header_trailer) then trailer ();
+      if (!header_trailer) then Output.header (); 
+      Output.make_index (); 
+      if (!header_trailer) then Output.trailer ();
       close_out_file()
     end;
     if (!toc && !target_language=HTML) then begin
       open_out_file "toc.html"; 
       page_title := (if !title <> "" then !title else "Table of contents");
-      if (!header_trailer) then header ();
+      if (!header_trailer) then Output.header ();
       if !title <> "" then printf "<h1>%s</h1>\n" !title;
-      make_toc (); 
-      if (!header_trailer) then trailer ();
+      Output.make_toc (); 
+      if (!header_trailer) then Output.trailer ();
       close_out_file()
     end 
       (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
 
+let read_glob x =
+  match x with
+    | Vernac_file (f,m) ->   
+	let glob = (Filename.chop_extension f) ^ ".glob" in
+	  (try
+	      Vernac_file (f, Index.read_glob glob)
+	    with _ -> 
+	      eprintf "Warning: file %s cannot be opened; links will not be available\n" glob;
+	      x)
+  | Latex_file _ -> x
 
 let index_module = function
-  | Vernac_file (_,m) -> Index.add_module m
+  | Vernac_file (f,m) ->   
+      Index.add_module m
   | Latex_file _ -> ()
       
 let produce_document l =
-  List.iter index_module l;
   (if !target_language=HTML then
     let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
     let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
       copy src dst);
   (if !target_language=LaTeX then
-    let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
-    let dst = if !output_dir <> "" then 
-      Filename.concat !output_dir "coqdoc.sty" 
-    else "coqdoc.sty" in
-      copy src dst);
+      let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
+      let dst = if !output_dir <> "" then 
+	  Filename.concat !output_dir "coqdoc.sty" 
+	else "coqdoc.sty" in
+	copy src dst);
+  let l = List.map read_glob l in
+  List.iter index_module l;
   match !out_to with
     | StdOut -> 
 	Cdglobals.out_channel := stdout;
@@ -446,51 +450,64 @@ let produce_document l =
 	gen_mult_files l
 	  
 let produce_output fl =
-  if not (!dvi || !ps) then begin
+  if not (!dvi || !ps || !pdf) then 
     produce_document fl
-  end else begin
-    let texfile = temp_file "coqdoc" ".tex" in
-    let basefile = chop_suffix texfile ".tex" in
-      open_out_file texfile;
-      produce_document fl;
-      let command = 
-	let file = basename texfile in
-	let file = 
-	  if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
+  else 
+    begin
+      let texfile = Filename.temp_file "coqdoc" ".tex" in
+      let basefile = Filename.chop_suffix texfile ".tex" in
+      let final_out_to = !out_to in
+	out_to := File texfile;
+	output_dir := (Filename.dirname texfile);
+	produce_document fl;
+	
+	let latexexe = if !pdf then "pdflatex" else "latex" in
+	let latexcmd = 
+	  let file = Filename.basename texfile in
+	  let file = 
+	    if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
+	  in
+	    sprintf "%s %s && %s %s 1>&2 %s" latexexe file latexexe file (if !quiet then "> /dev/null" else "")
 	in
-	  sprintf "(latex %s && latex %s) 1>&2 %s" file file
-	    (if !quiet then "> /dev/null" else "")
-      in
-      let res = locally (dirname texfile) Sys.command command in
-	if res <> 0 then begin
-	  eprintf "Couldn't run LaTeX successfully\n"; 
-	  clean_and_exit basefile res
-	end;
-	let dvifile = basefile ^ ".dvi" in
-	  if !dvi then begin
-	    if !output_file <> "" then 
-	      (* we cannot use Sys.rename accross file systems *)
-	      copy dvifile !output_file 
-	    else 
-	      cat dvifile
-	  end;
-	  if !ps then begin
-	    let psfile = 
-	      if !output_file <> "" then !output_file else basefile ^ ".ps" 
-	    in
-	    let command = 
-	      sprintf "dvips %s -o %s %s" dvifile psfile 
-		(if !quiet then "> /dev/null 2>&1" else "")
-	    in
-	    let res = Sys.command command in
-	      if res <> 0 then begin
-		eprintf "Couldn't run dvips successfully\n"; 
-		clean_and_exit basefile res
+	let res = locally (Filename.dirname texfile) Sys.command latexcmd in
+	  if res <> 0 then begin
+	      eprintf "Couldn't run LaTeX successfully\n"; 
+	      clean_and_exit basefile res
+	    end;
+	  
+	  let dvifile = basefile ^ ".dvi" in
+	    if !dvi then 
+	      begin
+		match final_out_to with
+		  | MultFiles | StdOut -> cat dvifile
+		  | File f -> copy dvifile f
 	      end;
-	      if !output_file = "" then cat psfile
-	  end;
-	  clean_temp_files basefile
-  end
+	  let pdffile = basefile ^ ".pdf" in
+	    if !pdf then 
+            begin
+	        match final_out_to with
+		  | MultFiles | StdOut -> cat pdffile
+		  | File f -> copy pdffile f
+	    end;
+	    if !ps then begin
+	        let psfile = basefile ^ ".ps" 
+		in
+		let command = 
+		  sprintf "dvips %s -o %s %s" dvifile psfile 
+		    (if !quiet then "> /dev/null 2>&1" else "")
+		in
+		let res = Sys.command command in
+		  if res <> 0 then begin
+		      eprintf "Couldn't run dvips successfully\n"; 
+		      clean_and_exit basefile res
+		    end;
+		  match final_out_to with
+		    | MultFiles | StdOut -> cat psfile
+		    | File f -> copy psfile f
+	      end;
+	 
+	    clean_temp_files basefile
+    end
 
 
 (*s \textbf{Main program.} Print the banner, parse the command line,
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 2d0bc6c2..93414f22 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 10248 2007-10-23 13:02:56Z notin $ i*)
+(*i $Id: output.ml 11154 2008-06-19 18:42:19Z msozeau $ i*)
 
 open Cdglobals
 open Index
@@ -31,28 +32,44 @@ let build_table l =
 
 let is_keyword = 
   build_table
-    [ "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
-      "CoInductive"; "Defined"; "Definition"; 
-      "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
+    [ "AddPath"; "Axiom"; "Chapter"; "Check"; "CoFixpoint";
+      "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
+      "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
-      "Immediate"; "Implicit"; "Import"; "Inductive"; 
+      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; 
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
-      "Module"; "Module Type"; "Declare Module";
+      "Module"; "Module Type"; "Declare Module"; "Include";
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
-      "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
-      "Set"; "Unset"; "Variable"; "Variables"; 
+      "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
+      "Set"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
-      "Delimit"; "Bind"; "Open"; "Scope";
-      "Boxed"; "Unboxed";
-      "Arguments";
+      "Delimit"; "Bind"; "Open"; "Scope"; 
+      "Boxed"; "Unboxed"; "Inline";
+      "Arguments"; "Add"; "Strict";
+      "Typeclasses"; "Instance"; "Class"; "Instantiation";
       (* Program *)
-      "Program Definition"; "Program Fixpoint"; "Program Lemma";
+      "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
+      "Program Instance";
       (*i (* coq terms *) *)
-	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="
+	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; 
+	"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"
        ]
 
+let is_tactic = 
+  build_table
+    [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite";
+      "destruct"; "induction"; "elim"; "dependent"; 
+      "generalize"; "clear"; "rename"; "move"; "set"; "assert";
+      "cut"; "assumption"; "exact"; "split"; "try"; "discriminate";
+      "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
+      "reflexivity"; "symmetry"; "transitivity";
+      "replace"; "setoid_replace"; "inversion"; "inversion_clear";
+      "pattern"; "intuition"; "congruence";
+      "trivial"; "exact"; "tauto"; "firstorder"; "ring";
+      "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ]
+
 (*s Current Coq module *)
 
 let current_module = ref ""
@@ -78,6 +95,7 @@ let remove_printing_token = Hashtbl.remove token_pp
 let _ = List.iter 
 	  (fun (s,l) -> Hashtbl.add token_pp s (Some l, None))
 	  [ "*" ,  "\\ensuremath{\\times}";
+	    "|", "\\ensuremath{|}";
 	    "->",  "\\ensuremath{\\rightarrow}";
 	    "->~",  "\\ensuremath{\\rightarrow\\lnot}";
 	    "->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}";
@@ -153,6 +171,12 @@ module Latex = struct
     | _ -> 
 	output_char c
 
+  let label_char c = match c with
+    | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
+    | '^' | '~' -> ()
+    | _ -> 
+	output_char c
+
   let latex_char = output_char
   let latex_string = output_string
 
@@ -162,9 +186,14 @@ module Latex = struct
   let raw_ident s =
     for i = 0 to String.length s - 1 do char s.[i] done
 
+  let label_ident s =
+    for i = 0 to String.length s - 1 do label_char s.[i] done
+
   let start_module () = 
     if not !short then begin
-      printf "\\coqdocmodule{"; 
+      printf "\\coqlibrary{"; 
+      label_ident !current_module; 
+      printf "}{";
       raw_ident !current_module; 
       printf "}\n\n"
     end
@@ -192,11 +221,53 @@ module Latex = struct
     with Not_found -> 
       f tok
 
-  let ident s _ = 
+  let module_ref m s = 
+    printf "\\moduleid{%s}{" m; raw_ident s; printf "}"
+      (*i
+    match find_module m with
+    | Local ->
+	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
+    | Coqlib when !externals ->
+	let m = Filename.concat !coqlib m in
+	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
+    | Coqlib | Unknown ->
+	raw_ident s
+    i*)
+
+  let ident_ref m fid typ s =
+    let id = if fid <> "" then (m ^ "." ^ fid) else m in
+    match find_module m with
+      | Local ->
+	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
+      | Coqlib when !externals ->
+	  let _m = Filename.concat !coqlib m in
+	    printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
+      | Coqlib | Unknown ->
+	  raw_ident s
+
+  let defref m id ty s =
+    printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}"
+
+  let ident s loc = 
     if is_keyword s then begin
       printf "\\coqdockw{"; raw_ident s; printf "}"
     end else begin
-      printf "\\coqdocid{"; raw_ident s; printf "}"
+      begin
+	try
+	  (match Index.find !current_module loc with
+	     | Def (fullid,typ) -> 
+		 defref !current_module 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 "\\coqdocid{"; raw_ident s; printf "}")
+	with Not_found ->
+	  if is_tactic s then begin
+	    printf "\\coqdoctac{"; raw_ident s; printf "}"
+	  end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end
+      end
     end
 
   let ident s l = with_latex_printing (fun s -> ident s l) s
@@ -271,31 +342,51 @@ end
 module Html = struct
 
   let header () =
-    if !header_trailer then begin
-      printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
-      printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
-      printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
-      printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset;
-      printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n";
-      printf "<title>%s</title>\n</head>\n\n" !page_title;
-      printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
-      printf "<div id=\"main\">\n\n"
-    end
+    if !header_trailer then
+      if !header_file_spec then
+	let cin = Pervasives.open_in !header_file in
+	  try 
+	    while true do 
+	      let s = Pervasives.input_line cin in 
+		printf "%s\n" s
+	    done
+	  with End_of_file -> Pervasives.close_in cin
+      else
+	begin
+	  printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
+	  printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
+	  printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
+	  printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset;
+	  printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n";
+	  printf "<title>%s</title>\n</head>\n\n" !page_title;
+	  printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
+	  printf "<div id=\"main\">\n\n"
+	end
 
   let self = "http://coq.inria.fr"
 
   let trailer () =
     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/>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
+    if !header_trailer then 
+      if !footer_file_spec then
+	let cin = Pervasives.open_in !footer_file in
+	  try 
+	    while true do 
+	      let s = Pervasives.input_line cin in 
+		printf "%s\n" s
+	    done
+	  with End_of_file -> Pervasives.close_in cin
+      else
+	begin
+	  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
 
   let start_module () = 
     if not !short then begin
-      (* add_toc_entry (Toc_library !current_module); *)
+      add_toc_entry (Toc_library !current_module);
       printf "<h1 class=\"libtitle\">Library %s</h1>\n\n" !current_module
     end
 
@@ -338,14 +429,15 @@ module Html = struct
 	raw_ident s
     i*)
 
-  let ident_ref m fid s = match find_module m with
-    | Local ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
-    | Coqlib when !externals ->
-	let m = Filename.concat !coqlib m in
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
-    | Coqlib | Unknown ->
-	raw_ident s
+  let ident_ref m fid s = 
+    match find_module m with
+      | Local ->
+	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
+      | Coqlib when !externals ->
+	  let m = Filename.concat !coqlib m in
+	    printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
+      | Coqlib | Unknown ->
+	  raw_ident s
 
   let ident s loc = 
     if is_keyword s then begin
@@ -360,9 +452,9 @@ module Html = struct
 		 printf "<a name=\"%s\"></a>" fullid; raw_ident s
              | Mod (m,s') when s = s' ->
 		 module_ref m s
-	     | Ref (m,fullid) -> 
+	     | Ref (m,fullid,ty) -> 
 		 ident_ref m fullid s
-	     | Mod _ | Ref _ ->
+	     | Mod _ ->
 		 raw_ident s)
 	with Not_found ->
 	  raw_ident s
@@ -429,17 +521,6 @@ module Html = struct
 
   let rule () = printf "<hr/>\n"
 
-  let entry_type = function
-    | Library -> "library"
-    | Module -> "module"
-    | Definition -> "definition"
-    | Inductive -> "inductive"
-    | Constructor -> "constructor"
-    | Lemma -> "lemma"
-    | Variable -> "variable"
-    | Axiom -> "axiom"
-    | TacticDefinition -> "tactic definition"
-
   (* make a HTML index from a list of triples (name,text,link) *)
   let index_ref i c =
     let idxc = sprintf "%s_%c" i.idx_name c in
@@ -465,7 +546,7 @@ module Html = struct
 	 if t = Library then 
 	   "[library]", m ^ ".html"
 	 else
-	   sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (entry_type t) m m ,
+	   sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
 	 sprintf "%s.html#%s" m s)
 
   let format_bytype_index = function
@@ -548,8 +629,8 @@ module Html = struct
 	  item n; 
 	  printf "<a href=\"%s\">" r; f (); printf "</a>\n"
     in
-    Queue.iter make_toc_entry toc_q;
-    stop_item ();
+      Queue.iter make_toc_entry toc_q;
+      stop_item ();
 
 end
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index e16c7979..8be3e0b0 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,28 +7,24 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 10248 2007-10-23 13:02:56Z notin $ i*)
+(*i $Id: pretty.mll 11154 2008-06-19 18:42:19Z msozeau $ i*)
 
 (*s Utility functions for the scanners *)
 
 {
-
-  open Cdglobals
   open Printf
-  open Index
   open Lexing 
-  open Output
 
   (* count the number of spaces at the beginning of a string *)
   let count_spaces s =
     let n = String.length s in
     let rec count c i = 
-      if i == n then c else match s.[i] with
+      if i == n then c,i else match s.[i] with
 	| '\t' -> count (c + (8 - (c mod 8))) (i + 1)
 	| ' ' -> count (c + 1) (i + 1)
-	| _ -> c
+	| _ -> c,i
     in
-    count 0 0
+      count 0 0
 
   let count_dashes s =
     let c = ref 0 in
@@ -52,6 +49,11 @@
     in
     count 0 (String.index s '*')
 
+  let strip_eol s =
+    let eol = s.[String.length s - 1] = '\n' in
+    (eol, if eol then String.sub s 1 (String.length s - 1) else s)
+
+
   let formatted = ref false
   let brackets = ref 0
 
@@ -69,22 +71,22 @@
   let state_stack = Stack.create ()
 
   let save_state () = 
-    Stack.push { st_gallina = !gallina; st_light = !light } state_stack
+    Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack
 
   let restore_state () =
     let s = Stack.pop state_stack in
-    gallina := s.st_gallina;
-    light := s.st_light
+    Cdglobals.gallina := s.st_gallina;
+    Cdglobals.light := s.st_light
       
   let without_ref r f x = save_state (); r := false; f x; restore_state ()
 
-  let without_gallina = without_ref gallina
+  let without_gallina = without_ref Cdglobals.gallina
 
-  let without_light = without_ref light
+  let without_light = without_ref Cdglobals.light
 
   let show_all f = without_gallina (without_light f)
 
-  let begin_show () = save_state (); gallina := false; light := false
+  let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
   let end_show () = restore_state ()
 
   (* Reset the globals *)
@@ -163,15 +165,20 @@
 
 let space = [' ' '\t']
 let space_nl = [' ' '\t' '\n' '\r']
+let nl = "\r\n" | '\n'
 
 let firstchar = 
   ['A'-'Z' 'a'-'z' '_' 
   (* iso 8859-1 accents *) 
   '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+  '\194' '\185' |
   (* utf-8 latin 1 supplement *) 
   '\195' ['\128'-'\191'] |
   (* utf-8 letterlike symbols *) 
-  '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+  '\206' ['\177'-'\183'] |
+  '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
+    | '\129' [ '\176'-'\187' ] (* superscripts *)
+    | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
 let identchar = 
   firstchar | ['\'' '0'-'9' '@' ]
 let id = firstchar identchar*
@@ -186,8 +193,9 @@ let symbolchar_no_brackets =
   (* utf-8 symbols *) 
   '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
 let symbolchar = symbolchar_no_brackets | '[' | ']'
+let token_no_brackets = symbolchar_no_brackets+
 let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
-
+let printing_token = (token | id)+
 
 let thm_token = 
   "Theorem" 
@@ -202,6 +210,7 @@ let thm_token =
 let def_token = 
   "Definition" 
   | "Let" 
+  | "Class"
   | "SubClass" 
   | "Example"
   | "Local" 
@@ -209,11 +218,10 @@ let def_token =
   | "CoFixpoint" 
   | "Record" 
   | "Structure" 
+  | "Instance"
   | "Scheme"
   | "Inductive"
   | "CoInductive"
-  | "Program" space+ "Definition"
-  | "Program" space+ "Fixpoint"
 
 let decl_token = 
   "Hypothesis" 
@@ -224,6 +232,8 @@ let decl_token =
 
 let gallina_ext =
   "Module" 
+  | "Include" space+ "Type"
+  | "Include"
   | "Declare" space+ "Module"
   | "Transparent"
   | "Opaque"
@@ -235,6 +245,11 @@ let gallina_ext =
   | "Infix"
   | "Tactic" space+ "Notation"
   | "Reserved" space+ "Notation"
+  | "Section"
+  | "Context"
+  | "Variable" 's'?
+  | ("Hypothesis" | "Hypotheses")
+  | "End"
 
 let commands = 
   "Pwd"
@@ -254,6 +269,12 @@ let commands =
   | "Check"
   | "Type"
 
+  | "Section"
+  | "Chapter"
+  | "Variable" 's'?
+  | ("Hypothesis" | "Hypotheses")
+  | "End"
+
 let extraction = 
   "Extraction"
   | "Recursive" space+ "Extraction" 
@@ -261,6 +282,12 @@ let extraction =
 
 let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
 
+let prog_kw =
+  "Program" space+ gallina_kw
+  | "Obligation"
+  | "Obligations"
+  | "Solve"
+
 let gallina_kw_to_hide =
   "Implicit"
   | "Ltac"
@@ -275,11 +302,6 @@ let gallina_kw_to_hide =
   | "Transparent"
   | "Opaque"
   | ("Declare" space+ ("Morphism" | "Step") )
-  | "Section"
-  | "Chapter"
-  | "Variable" 's'?
-  | ("Hypothesis" | "Hypotheses")
-  | "End"
   | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
   | "Declare" space+ ("Left" | "Right") space+ "Step" 
 
@@ -294,10 +316,10 @@ let section = "*" | "**" | "***" | "****"
 
 let item_space = "    "
 
-let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* '\n'
-let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* '\n'
-let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* '\n'
-let end_show = "(*" space* "end" space+ "show" space* "*)" space* '\n'
+let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl
+let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl
+let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl
+let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl
 (*
 let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
 let end_verb = "(*" space* "end" space+ "verb" space* "*)"
@@ -308,16 +330,16 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 (*s Scanning Coq, at beginning of line *)
 
 rule coq_bol = parse
-  | space* '\n'+
-      { empty_line_of_code (); coq_bol lexbuf }
+  | space* nl+
+      { Output.empty_line_of_code (); coq_bol lexbuf }
   | space* "(**" space_nl
-      { end_coq (); start_doc (); 
+      { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
-	  end_doc (); start_coq (); 
+	  Output.end_doc (); Output.start_coq (); 
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | space* "Comments" space_nl
-      { end_coq (); start_doc (); comments lexbuf; end_doc (); 
-	start_coq (); coq lexbuf }
+      { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc (); 
+	Output.start_coq (); coq lexbuf }
   | space* begin_hide
       { skip_hide lexbuf; coq_bol lexbuf }
   | space* begin_show
@@ -326,28 +348,38 @@ rule coq_bol = parse
       { end_show (); coq_bol lexbuf }
   | 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 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 }
+	  if !Cdglobals.light && section_or_end s then 
+	    let eol = skip_to_dot lexbuf in
+	      if eol then (Output.line_break (); coq_bol lexbuf) else coq lexbuf
+	  else 
+	    begin
+	      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); 
+		  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 s = String.sub s nbsp (String.length s - nbsp)  in
-	  indentation nbsp;
-	  ident s (lexeme_start lexbuf + nbsp); 
+	let nbsp,isp = count_spaces s in
+	let s = String.sub s isp (String.length s - isp)  in
+	  Output.indentation nbsp;
+	  Output.ident s (lexeme_start lexbuf + isp); 
 	  let eol= body lexbuf in
 	    if eol then coq_bol lexbuf else coq lexbuf }
-  | space* "(**" space+ "printing" space+ (identifier | token) space+
+  | space* prog_kw
+      { let s = lexeme lexbuf in 
+	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); 
+	    let eol= body lexbuf in
+	      if eol then coq_bol lexbuf else coq lexbuf }
+
+  | space* "(**" space+ "printing" space+ printing_token space+
       { let tok = lexeme lexbuf in
-	let s = printing_token lexbuf in
+	let s = printing_token_body lexbuf in
 	  add_printing_token tok s;
 	  coq_bol lexbuf }
   | space* "(**" space+ "printing" space+
@@ -366,13 +398,13 @@ rule coq_bol = parse
 	coq_bol lexbuf }
   | space* "(*"
       { let eol = comment lexbuf in
-	  if eol then begin line_break(); coq_bol lexbuf end else coq lexbuf }
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | eof 
       { () }
   | _
       { let eol = 
-	  if not !gallina then 
-	    begin backtrack lexbuf; indentation 0; body_bol lexbuf end 
+	  if not !Cdglobals.gallina then 
+	    begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end 
 	  else 
 	    skip_to_dot lexbuf 
 	in
@@ -381,141 +413,148 @@ rule coq_bol = parse
 (*s Scanning Coq elsewhere *)
 
 and coq = parse
-  | "\n" 
-      { line_break(); coq_bol lexbuf }
+  | nl 
+      { Output.line_break(); coq_bol lexbuf }
   | "(**" space_nl
-      { end_coq (); start_doc (); 
+      { Output.end_coq (); Output.start_doc (); 
 	let eol = doc_bol lexbuf in
-	  end_doc (); start_coq (); 
+	  Output.end_doc (); Output.start_coq (); 
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | "(*"
       { let eol = comment lexbuf in
-	  if eol then begin line_break(); coq_bol lexbuf end 
+	  if eol then begin Output.line_break(); coq_bol lexbuf end 
           else coq lexbuf
       }
-  | '\n'+ space* "]]"
-      { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end }
+  | nl+ space* "]]"
+      { if not !formatted then begin Output.symbol (lexeme lexbuf); coq lexbuf end }
   | eof 
       { () }
   | gallina_kw_to_hide
       { let s = lexeme lexbuf in
-	  if !light && section_or_end s then 
+	  if !Cdglobals.light && section_or_end s then 
 	    begin 
 	      let eol = skip_to_dot lexbuf in
 		if eol then coq_bol lexbuf else coq lexbuf 
 	    end 
 	  else 
 	    begin
-	      ident s (lexeme_start lexbuf); 
+	      Output.ident s (lexeme_start lexbuf); 
 	      let eol=body lexbuf in 
 		if eol then coq_bol lexbuf else coq lexbuf
 	    end }
   | gallina_kw
       { let s = lexeme lexbuf in 
-	  ident s (lexeme_start lexbuf); 
+	  Output.ident s (lexeme_start lexbuf); 
 	let eol = body lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
-  | space+ { char ' '; coq lexbuf }
+  | prog_kw
+      { let s = lexeme lexbuf in 
+	  Output.ident s (lexeme_start lexbuf); 
+	let eol = body lexbuf in
+	  if eol then coq_bol lexbuf else coq lexbuf }
+  | space+ { Output.char ' '; coq lexbuf }
   | eof 
       { () }
-  | _ { let eol = 
-	  if not !gallina then 
-	    begin backtrack lexbuf; indentation 0; body lexbuf end 
+  | _ {	let eol = 
+	  if not !Cdglobals.gallina then 
+	    begin backtrack lexbuf; Output.indentation 0; body lexbuf end 
 	  else 
-	    skip_to_dot lexbuf 
+	    let eol = skip_to_dot lexbuf in
+	      if eol then Output.line_break (); eol
 	in 
 	  if eol then coq_bol lexbuf else coq lexbuf}
       
 (*s Scanning documentation, at beginning of line *)
-      
+
 and doc_bol = parse
-  | space* "\n" '\n'*
-      { paragraph (); doc_bol lexbuf }
-  | space* section [^')'] ([^'\n' '*'] | '*' [^'\n'')'])*
-{ let lev, s = sec_title (lexeme lexbuf) in 
-    section lev (fun () -> ignore (doc (from_string s))); 
-    doc lexbuf }
-| space* '-'+
-     { let n = count_dashes (lexeme lexbuf) in
-	 if n >= 4 then rule () else item n;
-	 doc lexbuf }
-| "<<" space*
-      { start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
+  | 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
+          Output.section lev (fun () -> ignore (doc (from_string s)));
+	  if eol then doc_bol lexbuf else doc lexbuf }
+  | space* '-'+
+      { let n = count_dashes (lexeme lexbuf) in
+	if n >= 4 then Output.rule () else Output.item n;
+        doc lexbuf }
+  | "<<" space*
+      { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
   | eof 
-      { false }
+      { true }
   | _ 
       { backtrack lexbuf; doc lexbuf }
 
 (*s Scanning documentation elsewhere *)
 
 and doc = parse
-  | "\n"
-      { char '\n'; doc_bol lexbuf }
+  | nl
+      { Output.char '\n'; doc_bol lexbuf }
   | "["
       { brackets := 1; 
-	start_inline_coq (); escaped_coq lexbuf; end_inline_coq ();
+	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
 	doc lexbuf }
-  | "[[" '\n' space*
-      { formatted := true; line_break (); start_inline_coq ();
-	indentation (count_spaces (lexeme lexbuf)); 
+  | "[[" nl space*
+      { formatted := true; Output.line_break (); Output.start_inline_coq ();
+	Output.indentation (fst (count_spaces (lexeme lexbuf))); 
 	let eol = body_bol lexbuf in 
-	  end_inline_coq (); formatted := false;
+	  Output.end_inline_coq (); formatted := false;
 	  if eol then doc_bol lexbuf else doc lexbuf}
-  | '*'* "*)" space* '\n'
+  | '*'* "*)" space* nl
       { true }
   | '*'* "*)"
       { false }
   | "$"
-      { start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
+      { Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
   | "$$"
-      { char '$'; doc lexbuf }
+      { Output.char '$'; doc lexbuf }
   | "%"
       { escaped_latex lexbuf; doc lexbuf }
   | "%%"
-      { char '%'; doc lexbuf }
+      { Output.char '%'; doc lexbuf }
   | "#"
       { escaped_html lexbuf; doc lexbuf }
   | "##"
-      { char '#'; doc lexbuf }
+      { Output.char '#'; doc lexbuf }
   | eof 
       { false }
   | _ 
-      { char (lexeme_char lexbuf 0); doc lexbuf }
+      { Output.char (lexeme_char lexbuf 0); doc lexbuf }
 
 (*s Various escapings *)
 
 and escaped_math_latex = parse
-  | "$" { stop_latex_math () }
-  | eof { stop_latex_math () }
-  | _   { latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
+  | "$" { Output.stop_latex_math () }
+  | eof { Output.stop_latex_math () }
+  | _   { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
 
 and escaped_latex = parse
   | "%" { () }
   | eof { () }
-  | _   { latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
+  | _   { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
 
 and escaped_html = parse
   | "#" { () }
   | "&#"
-        { html_char '&'; html_char '#'; escaped_html lexbuf }
+        { Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf }
   | "##"
-        { html_char '#'; escaped_html lexbuf }
+        { Output.html_char '#'; escaped_html lexbuf }
   | eof { () }
-  | _   { html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
+  | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
 and verbatim = parse
-  | "\n>>" { verbatim_char '\n'; stop_verbatim () }
-  | eof { stop_verbatim () }
-  | _ { verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
+  | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
+  | eof { Output.stop_verbatim () }
+  | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
 
 (*s Coq, inside quotations *)
 
 and escaped_coq = parse
   | "]"
       { decr brackets; 
-	if !brackets > 0 then begin char ']'; escaped_coq lexbuf end }
+	if !brackets > 0 then begin Output.char ']'; escaped_coq lexbuf end }
   | "["
-      { incr brackets; char '['; escaped_coq lexbuf }
+      { incr brackets; Output.char '['; escaped_coq lexbuf }
   | "(*"
       { ignore (comment lexbuf); escaped_coq lexbuf }
   | "*)"
@@ -524,18 +563,18 @@ and escaped_coq = parse
       { () }
   | token_brackets
       { let s = lexeme lexbuf in
-	symbol s;
+	Output.symbol s;
 	escaped_coq lexbuf }
   | (identifier '.')* identifier
-      { ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
+      { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
   | _ 
-      { char (lexeme_char lexbuf 0); escaped_coq lexbuf }
+      { Output.char (lexeme_char lexbuf 0); escaped_coq lexbuf }
 
 (*s Coq "Comments" command. *)
 
 and comments = parse
   | space_nl+ 
-      { char ' '; comments lexbuf }
+      { Output.char ' '; comments lexbuf }
   | '"' [^ '"']* '"' 
       { let s = lexeme lexbuf in
 	let s = String.sub s 1 (String.length s - 2) in
@@ -547,61 +586,79 @@ and comments = parse
   | eof 
       { () }
   | _   
-      { char (lexeme_char lexbuf 0); comments lexbuf }
+      { Output.char (lexeme_char lexbuf 0); comments lexbuf }
 
 (*s Skip comments *)
 
 and comment = parse
-  | "(*" { ignore (comment lexbuf); comment lexbuf }
-  | "*)" space* '\n'+ { true }
+  | "(*" { comment lexbuf }
+  | "*)" space* nl { true }
   | "*)" { false }
   | eof  { false }
   | _    { comment lexbuf }
 
 and skip_to_dot = parse
-  | '.' space* '\n' { true }
+  | '.' space* nl { true }
   | eof | '.' space+ { false}
   | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
   | _ { skip_to_dot lexbuf }
 
 and body_bol = parse
   | space+
-      { indentation (count_spaces (lexeme lexbuf)); body lexbuf }
+      { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
   | _ { backtrack lexbuf; body lexbuf }
 
 and body = parse
-  | '\n' {line_break(); body_bol lexbuf}
-  | '\n'+ space* "]]"
-      { if not !formatted then begin symbol (lexeme lexbuf); body lexbuf end else true }
+  | nl {Output.line_break(); body_bol lexbuf}
+  | nl+ space* "]]"
+      { if not !formatted then begin Output.symbol (lexeme lexbuf); body lexbuf end else true }
   | eof { false }
-  | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true }      
-  | '.' space+ { char '.'; char ' '; false }
+  | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }      
+  | '.' space+ { Output.char '.'; Output.char ' '; false }
+  | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
   | "(*" { let eol = comment lexbuf in 
-	     if eol then begin line_break(); body_bol lexbuf end else body lexbuf }
+	     if eol 
+	     then begin Output.line_break(); body_bol lexbuf end
+	     else body lexbuf }
   | identifier 
       { let s = lexeme lexbuf in 
-	  ident s (lexeme_start lexbuf); 
+	  Output.ident s (lexeme_start lexbuf); 
 	  body lexbuf }
-  | token
+  | token_no_brackets
       { let s = lexeme lexbuf in
-	  symbol s; body lexbuf }
+	  Output.symbol s; body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
-	  char c; 
+	  Output.char c; 
           body lexbuf }
 
+and notation_bol = parse
+  | space+
+      { Output.indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf }
+  | _ { backtrack lexbuf; notation lexbuf }
+
+and notation = parse
+  | nl { Output.line_break(); notation_bol lexbuf }
+  | '"' { Output.char '"'; false }
+  | token
+      { let s = lexeme lexbuf in
+	  Output.symbol s; notation lexbuf }
+  | _ { let c = lexeme_char lexbuf 0 in 
+	  Output.char c; 
+          notation lexbuf }
+
 and skip_hide = parse
   | eof | end_hide { () }
   | _ { skip_hide lexbuf }
 
 (*s Reading token pretty-print *)
 
-and printing_token = parse
+and printing_token_body = parse
   | "*)" | eof 
 	{ let s = Buffer.contents token_buffer in 
 	  Buffer.clear token_buffer;
 	  s }
   | _   { Buffer.add_string token_buffer (lexeme lexbuf); 
-	  printing_token lexbuf }
+	  printing_token_body lexbuf }
 
 (*s Applying the scanners to files *)
 
@@ -609,11 +666,11 @@ and printing_token = parse
 
   let coq_file f m =
     reset ();
-    Index.scan_file f m;
-    start_module ();
+    Index.current_library := m;
+    Output.start_module ();
     let c = open_in f in
     let lb = from_channel c in
-    start_coq (); coq_bol lb; end_coq ();
+    Output.start_coq (); coq_bol lb; Output.end_coq ();
     close_in c
 
 }