Imported Upstream version 8.0pl1upstream/8.0pl1

11 files changed, 2460 insertions, 0 deletions

diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
new file mode 100644
index 00000000..2418b6e1
--- /dev/null
+++ b/tools/coqdoc/alpha.ml
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: alpha.ml,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+
+let norm_char c = match Char.uppercase c with
+  | '\192'..'\198' -> 'A'
+  | '\199' -> 'C'
+  | '\200'..'\203' -> 'E'
+  | '\204'..'\207' -> 'I'
+  | '\209' -> 'N'
+  | '\210'..'\214' -> 'O'
+  | '\217'..'\220' -> 'U'
+  | '\221' -> 'Y'
+  | c -> c
+
+let norm_string s =
+  let u = String.copy s in
+  for i = 0 to String.length s - 1 do
+    u.[i] <- norm_char s.[i]
+  done;
+  u
+
+let compare_char c1 c2 = match norm_char c1, norm_char c2 with
+  | ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2
+  | 'A'..'Z', _ -> -1
+  | _, 'A'..'Z' -> 1
+  | c1, c2 -> compare c1 c2
+
+let compare_string s1 s2 = 
+  let n1 = String.length s1 in
+  let n2 = String.length s2 in
+  let rec cmp i = 
+    if i == n1 || i == n2 then
+      n1 - n2
+    else
+      let c = compare_char s1.[i] s2.[i] in
+      if c == 0 then cmp (succ i) else c
+  in
+  cmp 0
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
new file mode 100644
index 00000000..46409c9a
--- /dev/null
+++ b/tools/coqdoc/alpha.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: alpha.mli,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+
+(* Alphabetic order. *)
+
+val compare_char : char -> char -> int
+val compare_string : string -> string -> int
+
+(* Alphabetic normalization. *)
+
+val norm_char : char -> char
+val norm_string : string -> string
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
new file mode 100644
index 00000000..7f7aa9aa
--- /dev/null
+++ b/tools/coqdoc/coqdoc.sty
@@ -0,0 +1,58 @@
+
+% This is coqdoc.sty, by Jean-Christophe Filliātre
+% This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc)
+%
+% You can modify the following macros to customize the appearance
+% of the document.
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{coqdoc}[2002/02/11]
+
+% Headings
+
+\usepackage{fancyhdr}
+\newcommand{\coqdocleftpageheader}{\thepage\ -- \today}
+\newcommand{\coqdocrightpageheader}{\today\ -- \thepage}
+\pagestyle{fancyplain}
+
+%BEGIN LATEX
+\plainheadrulewidth 0.4pt
+\plainfootrulewidth 0pt
+\lhead[\coqdocleftpageheader]{\leftmark}
+\rhead[\leftmark]{\coqdocrightpageheader}
+\cfoot{}
+%END LATEX
+
+% Hevea puts to much space with \medskip and \bigskip
+%HEVEA\renewcommand{\medskip}{}
+%HEVEA\renewcommand{\bigskip}{}
+
+% own name
+\newcommand{\coqdoc}{\textsf{coqdoc}}
+
+% pretty underscores (the package fontenc causes ugly underscores)
+%BEGIN LATEX
+\def\_{\kern.08em\vbox{\hrule width.35em height.6pt}\kern.08em}
+%END LATEX
+
+% macro for typesetting keywords
+\newcommand{\coqdockw}[1]{\textsf{#1}}
+
+% macro for typesetting identifiers
+\newcommand{\coqdocid}[1]{\textit{#1}}
+
+% newline and indentation 
+%BEGIN LATEX
+\newcommand{\coqdoceol}{\setlength\parskip{0pt}\par}
+\newcommand{\coqdocindent}[1]{\noindent\kern#1}
+%END LATEX
+%HEVEA\newcommand{\coqdoceol}{\begin{rawhtml}<BR>\end{rawhtml}}
+%HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}}
+
+% macro for typesetting the title of a module implementation
+\newcommand{\coqdocmodule}[1]{\section*{Module #1}\markboth{Module #1}{}}
+
+%HEVEA\newcommand{\lnot}{\coqwkw{not}}
+%HEVEA\newcommand{\lor}{\coqwkw{or}}
+%HEVEA\newcommand{\land}{\&}
+
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
new file mode 100644
index 00000000..60c21387
--- /dev/null
+++ b/tools/coqdoc/index.mli
@@ -0,0 +1,59 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: index.mli,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+
+type coq_module = string
+
+type loc = int
+
+type entry_type = 
+  | Library
+  | Module
+  | Definition
+  | Inductive
+  | Constructor
+  | Lemma
+  | Variable
+  | Axiom
+  | TacticDefinition
+
+type index_entry = 
+  | Def of string * entry_type
+  | Ref of coq_module * string
+  | Mod of coq_module * string
+
+val find : coq_module -> loc -> index_entry
+
+val add_module : coq_module -> unit
+
+type module_kind = Local | Coqlib | Unknown
+
+val find_module : coq_module -> module_kind
+
+(*s Scan identifiers introductions from a file *)
+
+val scan_file : string -> coq_module -> unit
+
+(*s Read globalizations from a file (produced by coqc -dump-glob) *)
+
+val read_glob : string -> unit
+
+(*s Indexes *)
+
+type 'a index = { 
+  idx_name : string;
+  idx_entries : (char * (string * 'a) list) list;
+  idx_size : int }
+
+val all_entries : unit -> 
+      (coq_module * entry_type) index *
+      (entry_type * coq_module index) list
+
+val map : (string -> 'a -> 'b) -> 'a index -> 'b index
+
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
new file mode 100644
index 00000000..799825ad
--- /dev/null
+++ b/tools/coqdoc/index.mll
@@ -0,0 +1,327 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: index.mll,v 1.2.2.1 2004/07/16 19:31:46 herbelin Exp $ i*)
+
+{
+
+open Filename
+open Lexing 
+open Printf
+
+type coq_module = string
+
+type loc = int
+
+type entry_type = 
+  | Library
+  | Module
+  | Definition
+  | Inductive
+  | Constructor
+  | Lemma
+  | Variable
+  | Axiom
+  | TacticDefinition
+
+type index_entry = 
+  | Def of string * entry_type
+  | Ref of coq_module * string
+  | Mod of coq_module * string
+
+let table = Hashtbl.create 97
+
+let current_module = ref ""
+
+let add_def loc ty id = Hashtbl.add table (!current_module, loc) (Def (id, ty))
+
+let add_ref m loc m' id = Hashtbl.add table (m, loc) (Ref (m', id))
+
+let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
+
+let find m l = Hashtbl.find table (m, l)
+
+let current_type = ref Library
+
+(* 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
+
+let modules = Hashtbl.create 97
+let local_modules = Hashtbl.create 97
+
+let add_module m =
+  let _,id = split_sp m in
+  Hashtbl.add modules id m;
+  Hashtbl.add local_modules m ()
+
+type module_kind = Local | Coqlib | Unknown
+
+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 
+    Local
+  else if coq_module m then
+    Coqlib
+  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_module (loc+i+1) (Hashtbl.find modules id) id
+  with Not_found -> 
+    ()
+
+(* Building indexes *)
+
+type 'a index = { 
+  idx_name : string;
+  idx_entries : (char * (string * 'a) list) list;
+  idx_size : int }
+		  
+let map f i = 
+  { i with idx_entries = 
+      List.map 
+	(fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l)) 
+	i.idx_entries }
+
+let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2
+
+let sort_entries el =
+  let t = Hashtbl.create 97 in
+  List.iter 
+    (fun c -> Hashtbl.add t c [])
+    ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N'; 
+     'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_'];  
+  List.iter 
+    (fun ((s,_) as e) -> 
+       let c = Alpha.norm_char s.[0] in 
+       let l = try Hashtbl.find t c with Not_found -> [] in
+       Hashtbl.replace t c (e :: l)) 
+    el;
+  let res = ref [] in
+  Hashtbl.iter 
+    (fun c l -> res := (c, List.sort compare_entries l) :: !res) t;
+  List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res
+    
+let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
+
+let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
+
+let type_name = function
+  | Library -> "library"
+  | Module -> "module"
+  | Definition -> "definition"
+  | Inductive -> "inductive"
+  | Constructor -> "constructor"
+  | Lemma -> "lemma"
+  | Variable -> "variable"
+  | Axiom -> "axiom"
+  | TacticDefinition -> "tactic"
+
+let all_entries () =
+  let gl = ref [] in
+  let add_g s m t = gl := (s,(m,t)) :: !gl in
+  let bt = Hashtbl.create 11 in
+  let add_bt t s m =
+    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 table;
+  Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
+  { idx_name = "global"; 
+    idx_entries = sort_entries !gl; 
+    idx_size = List.length !gl },
+  Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t; 
+				   idx_entries = sort_entries e; 
+				   idx_size = List.length e }) :: l) bt []
+
+}
+
+(*s Shortcuts for regular expressions. *)
+
+let space = 
+  [' ' '\010' '\013' '\009' '\012']
+let firstchar = 
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
+let identchar = 
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
+   '\'' '0'-'9']
+let ident = 
+  firstchar identchar*
+
+let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
+let end_hide = "(*" space* "end" space+ "hide" space* "*)"
+
+(*s Indexing entry point. *)
+
+rule traverse = parse
+  | "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
+      { current_type := Definition; index_ident lexbuf; fixpoint lexbuf;
+	traverse lexbuf }
+  | ("Lemma" | "Theorem") space
+      { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
+  | "Inductive" space
+      { current_type := Inductive; 
+	index_ident lexbuf; inductive lexbuf; traverse lexbuf }
+  | "Record" space
+      { current_type := Inductive; index_ident lexbuf; traverse lexbuf }
+  | "Module" (space+ "Type")? space
+      { current_type := Module; index_ident lexbuf; traverse lexbuf }
+(*i***
+  | "Variable" 's'? space
+      { current_type := Variable; index_idents lexbuf; traverse lexbuf }
+***i*)
+  | "Require" (space+ "Export")? space+ ident
+      { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf }
+  | begin_hide 
+      { skip_hide lexbuf; traverse lexbuf }
+  | "(*" 
+      { comment lexbuf; traverse lexbuf }
+  | '"'
+      { string lexbuf; traverse lexbuf }
+  | eof          
+      { () }
+  | _            
+      { traverse lexbuf }
+
+(*s Index one identifier. *)
+
+and index_ident = parse
+  | space+ 
+      { index_ident lexbuf }
+  | ident  
+      { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf) }
+  | eof    
+      { () }
+  | _      
+      { () }
+
+(*s Index identifiers separated by blanks and/or commas. *)
+
+and index_idents = parse
+  | space+ | ','
+      { index_idents lexbuf }
+  | ident  
+      { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf);
+	index_idents lexbuf }
+  | eof    
+      { () }
+  | _
+      { skip_until_point lexbuf }
+
+(*s Index identifiers in an inductive definition (types and constructors). *)
+
+and inductive = parse
+  | '|' | ":=" space* '|'? 
+      { current_type := Constructor; index_ident lexbuf; inductive lexbuf }
+  | "with" space
+      { current_type := Inductive; index_ident lexbuf; inductive lexbuf }
+  | '.'    
+      { () }
+  | eof    
+      { () }
+  | _      
+      { inductive lexbuf }
+
+(*s Index identifiers in a Fixpoint declaration. *)
+
+and fixpoint = parse
+  | "with" space
+      { index_ident lexbuf; fixpoint lexbuf }
+  | '.' 
+      { () }
+  | eof    
+      { () }
+  | _      
+      { fixpoint lexbuf }
+
+(*s Skip a possibly nested comment. *)
+
+and comment = parse
+  | "*)" { () }
+  | "(*" { comment lexbuf; comment lexbuf }
+  | '"'  { string lexbuf; comment lexbuf }
+  | eof  { eprintf " *** Unterminated comment while indexing" }
+  | _    { comment lexbuf }
+
+(*s Skip a constant string. *)
+
+and string = parse
+  | '"'  { () }
+  | eof  { eprintf " *** Unterminated string while indexing" }
+  | _    { string lexbuf }
+
+(*s Skip everything until the next dot. *)
+
+and skip_until_point = parse
+  | '.'  { () }
+  | eof  { () }
+  | _    { skip_until_point lexbuf }
+
+(*s Skip everything until [(* end hide *)] *)
+
+and skip_hide = parse
+  | eof | end_hide { () }
+  | _ { skip_hide lexbuf }
+
+{
+  
+  let read_glob f = 
+    let c = open_in f in
+    let cur_mod = ref "" in
+    try
+      while true do
+	let s = input_line c in
+	let n = String.length s in
+	if n > 0 then begin
+	  match s.[0] with
+	    | 'F' -> 
+		cur_mod := String.sub s 1 (n - 1)
+	    | 'R' ->
+		(try
+		   let i = String.index s ' ' in
+		   let loc = int_of_string (String.sub s 1 (i - 1)) in
+		   let sp = String.sub s (i + 1) (n - i - 1) in
+		   let m',id = split_sp sp in
+		   add_ref !cur_mod loc m' id
+		 with Not_found -> 
+		   ())
+	    | _ -> ()
+	end
+      done
+    with End_of_file -> 
+      close_in c
+
+  let scan_file f m = 
+    current_module := m;
+    let c = open_in f in
+    let lb = from_channel c in
+    traverse lb;
+    close_in c
+}
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
new file mode 100644
index 00000000..66d2a993
--- /dev/null
+++ b/tools/coqdoc/main.ml
@@ -0,0 +1,420 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: main.ml,v 1.4.2.1 2004/07/16 19:31:47 herbelin Exp $ 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 "./"
+ *  - function chop_prefix not useful anymore. Deleted.
+ *  - correct typo in usage message: "-R" -> "--R"
+ *  - shorten the definition of make_path
+ * This notice is made to comply with section 2.a of the GPLv2.
+ * It may be removed or abbreviated as far as I am concerned.
+ *)
+
+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 "  -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 "  -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 "";
+  prerr_endline 
+    "On-line documentation at http://www.lri.fr/~filliatr/coqdoc/\n";
+  exit 1
+
+(*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 
+    course). *)
+
+let banner () =
+  eprintf "This is coqdoc version %s, compiled on %s\n"
+    Coq_config.version Coq_config.compile_date;
+  flush stderr
+    
+
+(*s \textbf{Separation of files.} Files given on the command line are
+    separated according to their type, which is determined by their
+    suffix.  Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\
+    files have suffix \verb!.tex!. *)
+
+let check_if_file_exists f =
+  if not (Sys.file_exists f) then begin
+    eprintf "\ncoqdoc: %s: no such file\n" f;
+    exit 1
+  end
+
+let paths = ref []
+
+let add_path m l = paths := (m,l) :: !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 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 what_file f =
+  check_if_file_exists f;
+  if check_suffix f ".v" || check_suffix f ".g" then
+    Vernac_file (f, coq_module f)
+  else if 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
+
+(*s \textbf{Reading file names from a file.} 
+    File names may be given
+    in a file instead of being given on the command
+    line. [(files_from_file f)] returns the list of file names contained
+    in the file named [f]. These file names must be separated by spaces,
+    tabulations or newlines.
+ *)
+
+let files_from_file f =
+  let files_from_channel ch =
+    let buf = Buffer.create 80 in
+    let l = ref [] in
+    try
+      while true do
+	match input_char ch with
+	  | ' ' | '\t' | '\n' ->
+	      if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
+	      Buffer.clear buf
+	  | c -> 
+	      Buffer.add_char buf c
+      done; []
+    with End_of_file ->
+      List.rev !l
+  in
+  try
+    check_if_file_exists f;
+    let ch = open_in f in
+    let l = files_from_channel ch in
+    close_in ch;l
+  with Sys_error s -> begin
+    eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s;
+    exit 1
+  end
+
+(*s \textbf{Parsing of the command line.} *)
+
+let output_file = ref ""
+let dvi = ref false
+let ps = ref false
+
+let parse () =
+  let files = ref [] in
+  let add_file f = files := f :: !files in
+  let rec parse_rec = function
+    | [] -> ()
+
+    | ("-nopreamble" | "--nopreamble" | "--no-preamble"
+    |  "-bodyonly"   | "--bodyonly"   | "--body-only") :: rem ->
+	header_trailer := false; parse_rec rem
+    | ("-p" | "--preamble") :: s :: rem ->
+	push_in_preamble s; parse_rec rem
+    | ("-p" | "--preamble") :: [] ->
+	usage ()
+    | ("-noindex" | "--noindex" | "--no-index") :: rem ->
+	index := false; parse_rec rem
+    | ("-multi-index" | "--multi-index") :: rem ->
+	multi_index := true; parse_rec rem
+    | ("-toc" | "--toc" | "--table-of-contents") :: rem ->
+	toc := true; parse_rec rem
+    | ("-o" | "--output") :: f :: rem ->
+	output_file := f; parse_rec rem
+    | ("-o" | "--output") :: [] -> 
+	usage ()
+    | ("-d" | "--directory") :: dir :: rem ->
+	output_dir := dir; parse_rec rem
+    | ("-d" | "--directory") :: [] -> 
+	usage ()
+    | ("-s" | "--short") :: rem ->
+	short := true; parse_rec rem
+    | ("-l" | "-light" | "--light") :: rem ->
+	gallina := true; light := true; parse_rec rem
+    | ("-g" | "-gallina" | "--gallina") :: rem ->
+	gallina := true; parse_rec rem
+    | ("-t" | "-title" | "--title") :: s :: rem ->
+	title := s; parse_rec rem
+    | ("-t" | "-title" | "--title") :: [] ->
+	usage ()
+    | ("-latex" | "--latex") :: rem ->
+	Output.target_language := LaTeX; parse_rec rem
+    | ("-dvi" | "--dvi") :: rem ->
+	Output.target_language := LaTeX; dvi := true; parse_rec rem
+    | ("-ps" | "--ps") :: rem ->
+	Output.target_language := LaTeX; ps := true; parse_rec rem
+    | ("-html" | "--html") :: rem ->
+	Output.target_language := HTML; parse_rec rem
+    | ("-texmacs" | "--texmacs") :: rem ->
+	Output.target_language := TeXmacs; parse_rec rem
+
+    | ("-charset" | "--charset") :: s :: rem ->
+	Output.charset := s; parse_rec rem
+    | ("-charset" | "--charset") :: [] ->
+	usage ()
+    | ("-inputenc" | "--inputenc") :: s :: rem ->
+	Output.inputenc := s; parse_rec rem
+    | ("-inputenc" | "--inputenc") :: [] ->
+	usage ()
+    | ("-raw-comments" | "--raw-comments") :: rem ->
+	Output.raw_comments := true; parse_rec rem
+    | ("-latin1" | "--latin1") :: rem ->
+	Output.set_latin1 (); parse_rec rem
+    | ("-utf8" | "--utf8") :: rem ->
+	Output.set_utf8 (); parse_rec rem
+
+    | ("-q" | "-quiet" | "--quiet") :: rem ->
+	quiet := true; parse_rec rem
+
+    | ("-h" | "-help" | "-?" | "--help") :: rem ->
+	banner (); usage ()
+    | ("-v" | "-version" | "--version") :: _ ->
+	banner (); exit 0
+
+    | ("-vernac-file" | "--vernac-file") :: f :: rem -> 
+	check_if_file_exists f;
+	add_file (Vernac_file (f, coq_module f)); parse_rec rem
+    | ("-vernac-file" | "--vernac-file") :: [] ->
+	usage ()
+    | ("-tex-file" | "--tex-file") :: f :: rem -> 
+	add_file (Latex_file f); parse_rec rem
+    | ("-tex-file" | "--tex-file") :: [] ->
+	usage ()
+    | ("-files" | "--files" | "--files-from") :: f :: rem ->
+	List.iter (fun f -> add_file (what_file f)) (files_from_file f); 
+	parse_rec rem
+    | ("-files" | "--files") :: [] ->
+	usage ()
+
+    | "-R" :: path :: log :: rem -> 
+	add_path path log; parse_rec rem
+    | "-R" :: ([] | [_]) ->
+	usage ()
+    | ("-glob-from" | "--glob-from") :: f :: rem ->
+	Index.read_glob f; parse_rec rem
+    | ("-glob-from" | "--glob-from") :: [] ->
+	usage ()
+    | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
+	Output.externals := false; parse_rec rem
+    | ("--coqlib" | "-coqlib") :: u :: rem ->
+	Output.coqlib := u; parse_rec rem
+    | ("--coqlib" | "-coqlib") :: [] ->
+	usage ()
+
+    | f :: rem -> 
+	add_file (what_file f); parse_rec rem
+  in 
+  parse_rec (List.tl (Array.to_list Sys.argv));
+  List.rev !files
+
+
+(*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. *)
+
+let locally dir f x =
+  let cwd = Sys.getcwd () in
+  try
+    Sys.chdir dir; let y = f x in Sys.chdir cwd; y
+  with e ->
+    Sys.chdir cwd; raise e
+
+let clean_temp_files basefile =
+  let remove f = try Sys.remove f with _ -> () in
+  remove (basefile ^ ".tex");
+  remove (basefile ^ ".log");
+  remove (basefile ^ ".aux");
+  remove (basefile ^ ".dvi");
+  remove (basefile ^ ".ps");
+  remove (basefile ^ ".haux");
+  remove (basefile ^ ".html")
+
+let clean_and_exit file res = clean_temp_files file; exit res
+
+let cat file =
+  let c = open_in file in
+  try
+    while true do print_char (input_char c) done
+  with End_of_file ->
+    close_in c
+
+let copy src dst =
+  let cin = open_in src 
+  and cout = open_out dst in
+  try
+    while true do Pervasives.output_char cout (input_char cin) done
+  with End_of_file ->
+    close_in cin; close_out cout
+
+let produce_output fl =
+  if not (!dvi || !ps) then begin
+    if !output_file <> "" then set_out_file !output_file;
+    produce_document fl
+  end else begin
+    let texfile = temp_file "coqdoc" ".tex" in
+    let basefile = chop_suffix texfile ".tex" in
+    set_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 
+      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
+      end;
+      if !output_file = "" then cat psfile
+    end;
+    clean_temp_files basefile
+  end
+
+
+(*s \textbf{Main program.} Print the banner, parse the command line,
+    read the files and then call [produce_document] from module [Web]. *)
+
+let main () =
+  let files = parse () in
+  if not !quiet then banner ();
+  if List.length files > 0 then produce_output files
+
+let _ = Printexc.catch main ()
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
new file mode 100644
index 00000000..c10f3683
--- /dev/null
+++ b/tools/coqdoc/output.ml
@@ -0,0 +1,812 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: output.ml,v 1.7.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+
+open Index
+
+(*s Target language *)
+
+type target_language = LaTeX | HTML | TeXmacs
+
+let target_language = ref HTML
+
+(*s Low level output *)
+
+let out_channel = ref stdout
+let output_is_file = ref false
+let output_dir = ref ""
+
+let set_out_file f = 
+  let f = if !output_dir <> "" then Filename.concat !output_dir f else f in
+  out_channel := open_out f;
+  output_is_file := true
+
+let close () =
+  if !output_is_file then close_out !out_channel
+
+let output_char c = Pervasives.output_char !out_channel c
+
+let output_string s = Pervasives.output_string !out_channel s
+
+let printf s = Printf.fprintf !out_channel s
+
+let sprintf = Printf.sprintf
+
+let dump_file f =
+  let ch = open_in f in
+  try
+    while true do
+      Pervasives.output_char !out_channel (input_char ch)
+    done
+  with End_of_file -> close_in ch
+
+(*s Options *)
+
+let header_trailer = ref true
+let quiet = ref false
+let light = ref false
+let short = ref false
+let index = ref true
+let multi_index = ref false
+let toc = ref false
+let page_title = ref ""
+let title = ref ""
+let externals = ref true
+let coqlib = ref "http://coq.inria.fr/library/"
+let raw_comments = ref false
+
+let charset = ref ""
+let inputenc = ref ""
+let latin1 = ref false
+let utf8 = ref false
+
+let set_latin1 () =
+  charset := "iso-8859-1";
+  inputenc := "latin1";
+  latin1 := true
+
+let set_utf8 () =
+  charset := "utf-8";
+  inputenc := "utf8";
+  utf8 := true
+
+(*s Coq keywords *)
+
+let build_table l = 
+  let h = Hashtbl.create 101 in
+  List.iter (fun key ->Hashtbl.add h  key ()) l;
+  function s -> try Hashtbl.find h s; true with Not_found -> false
+
+let is_keyword = 
+  build_table
+    [ "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
+      "CoInductive"; "Defined"; "Definition"; 
+      "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
+      "Hypothesis"; "Hypotheses"; 
+      "Immediate"; "Implicit"; "Import"; "Inductive"; 
+      "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
+      "Module"; "Module Type"; "Declare Module";
+      "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
+      "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
+      "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
+      "Unset"; "Variable"; "Variables"; 
+      "Notation"; 
+      (*i (* correctness *)
+      "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if";
+      "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant";
+      "while"; i*)
+      (*i (* coq terms *)
+      "with"; "Case"; "Cases"; "Prop"; "Set"; "Type"; i*)
+       ]
+
+(*s Current Coq module *)
+
+let current_module = ref ""
+
+let set_module m = current_module := m; page_title := m
+
+(*s Common to both LaTeX and HTML *)
+
+let item_level = ref 0
+
+(*s Customized pretty-print *)
+
+let token_pp = Hashtbl.create 97
+
+let add_printing_token = Hashtbl.replace token_pp
+
+let find_printing_token tok = 
+  try Hashtbl.find token_pp tok with Not_found -> None, None
+
+let remove_printing_token = Hashtbl.remove token_pp
+
+(* predefined pretty-prints *)
+let _ = List.iter 
+	  (fun (s,l) -> Hashtbl.add token_pp s (Some l, None))
+	  [ "*" ,  "\\ensuremath{\\times}";
+	    "->",  "\\ensuremath{\\rightarrow}";
+	    "->~",  "\\ensuremath{\\rightarrow\\lnot}";
+	    "->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}";
+	    "<-",  "\\ensuremath{\\leftarrow}";
+	    "<->", "\\ensuremath{\\leftrightarrow}";
+	    "=>",  "\\ensuremath{\\Rightarrow}";
+	    "<=",  "\\ensuremath{\\le}";
+	    ">=",  "\\ensuremath{\\ge}";
+	    "<>",  "\\ensuremath{\\not=}";
+	    "~",   "\\ensuremath{\\lnot}";
+	    "/\\", "\\ensuremath{\\land}";
+	    "\\/", "\\ensuremath{\\lor}";
+	    "|-",  "\\ensuremath{\\vdash}";
+	    "forall", "\\ensuremath{\\forall}";
+	    "exists", "\\ensuremath{\\exists}";
+	  ]
+
+(*s Table of contents *)
+
+type toc_entry = 
+  | Toc_library of string
+  | Toc_section of int * (unit -> unit) * string
+
+let (toc_q : toc_entry Queue.t) = Queue.create ()
+
+let add_toc_entry e = Queue.add e toc_q
+
+let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r
+
+(*s LaTeX output *)
+
+module Latex = struct
+
+  (*s Latex preamble *)
+
+  let (preamble : string Queue.t) = Queue.create ()
+
+  let push_in_preamble s = Queue.add s preamble
+
+  let header () =
+    if !header_trailer then begin
+      printf "\\documentclass[12pt]{article}\n";
+      if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc;
+      printf "\\usepackage[T1]{fontenc}\n";
+      printf "\\usepackage{fullpage}\n";
+      printf "\\usepackage{coqdoc}\n";
+      Queue.iter (fun s -> printf "%s\n" s) preamble;
+      printf "\\begin{document}\n"
+    end;
+    output_string 
+      "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n";
+    output_string
+      "%% This file has been automatically generated with the command\n";
+    output_string "%% ";
+    Array.iter (fun s -> printf "%s " s) Sys.argv;
+    printf "\n";
+    output_string
+      "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"
+
+  let trailer () =
+    if !header_trailer then begin
+      printf "\\end{document}\n"
+    end
+
+  let char c = match c with
+    | '\\' -> 
+	printf "\\symbol{92}"
+    | '$' | '#' | '%' | '&' | '{' | '}' | '_' -> 
+	output_char '\\'; output_char c
+    | '^' | '~' -> 
+	output_char '\\'; output_char c; printf "{}"
+    | _ -> 
+	output_char c
+
+  let latex_char = output_char
+  let latex_string = output_string
+
+  let html_char _ = ()
+  let html_string _ = ()
+
+  let raw_ident s =
+    for i = 0 to String.length s - 1 do char s.[i] done
+
+  let start_module () = 
+    if not !short then begin
+      printf "\\coqdocmodule{"; 
+      raw_ident !current_module; 
+      printf "}\n\n"
+    end
+
+  let start_latex_math () = output_char '$'
+
+  let stop_latex_math () = output_char '$'
+
+  let start_verbatim () = printf "\\begin{verbatim}"
+
+  let stop_verbatim () = printf "\\end{verbatim}\n"
+
+  let indentation n = 
+    if n == 0 then 
+      printf "\\noindent\n"
+    else
+      let space = 0.5 *. (float n) in
+      printf "\\coqdocindent{%2.2fem}\n" space
+
+  let with_latex_printing f tok =
+    try 
+      (match Hashtbl.find token_pp tok with
+	 | Some s, _ -> output_string s
+	 | _ -> f tok)
+    with Not_found -> 
+      f tok
+
+  let ident s _ = 
+    if is_keyword s then begin
+      printf "\\coqdockw{"; raw_ident s; printf "}"
+    end else begin
+      printf "\\coqdocid{"; raw_ident s; printf "}"
+    end
+
+  let ident s l = with_latex_printing (fun s -> ident s l) s
+
+  let symbol = with_latex_printing raw_ident
+
+  let rec reach_item_level n = 
+    if !item_level < n then begin
+      printf "\n\\begin{itemize}\n\\item "; incr item_level;
+      reach_item_level n
+    end else if !item_level > n then begin
+      printf "\n\\end{itemize}\n"; decr item_level;
+      reach_item_level n
+    end
+
+  let item n =
+    let old_level = !item_level in
+    reach_item_level n;
+    if n <= old_level then printf "\n\\item "
+
+  let stop_item () = reach_item_level 0
+
+  let start_doc () = printf "\n\n\n\\noindent\n"
+
+  let end_doc () = stop_item (); printf "\n\n\n"
+
+  let start_coq () = ()
+
+  let end_coq () = ()
+
+  let start_code () = end_doc (); start_coq ()
+
+  let end_code () = end_coq (); start_doc ()
+
+  let section_kind = function
+    | 1 -> "\\section{"
+    | 2 -> "\\subsection{"
+    | 3 -> "\\subsubsection{"
+    | 4 -> "\\paragraph{"
+    | _ -> assert false
+
+  let section lev f =
+    stop_item ();
+    output_string (section_kind lev);
+    f ();
+    printf "}\n\n"
+
+  let rule () =
+    printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}"
+
+  let paragraph () = stop_item (); printf "\n\n\\medskip\n"
+
+  let line_break () = printf "\\coqdoceol\n"
+
+  let empty_line_of_code () = printf "\n\n\\medskip\n"
+
+  let start_inline_coq () = ()
+
+  let end_inline_coq () = ()
+
+  let make_index () = ()
+
+  let make_toc () = printf "\\tableofcontents\n"
+
+end
+
+
+(*s HTML output *)
+
+module Html = struct
+
+  let header () =
+    if !header_trailer then begin
+      printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
+      if !charset != "" then 
+	printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\">" !charset;
+      printf "<link rel=\"stylesheet\" href=\"style.css\" type=\"text/css\">";
+      printf "<title>%s</title>\n</head>\n\n" !page_title;
+      printf "<body>\n\n"
+    end
+
+  let self = "http://www.lri.fr/~filliatr/coqdoc/"
+
+  let trailer () =
+    if !index && !current_module <> "Index" then 
+      printf "<hr/><a href=\"index.html\">Index</a>";
+    if !header_trailer then begin
+      printf "<hr/><font size=\"-1\">This page has been generated by ";
+      printf "<a href=\"%s\">coqdoc</a></font>\n" self;
+      printf "</body>\n</html>"
+    end
+
+  let start_module () = 
+    if not !short then begin
+      (* add_toc_entry (Toc_library !current_module); *)
+      printf "<h1>Library %s</h1>\n\n" !current_module
+    end
+
+  let indentation n = for i = 1 to n do printf "&nbsp;" done
+
+  let line_break () = printf "<br/>\n"
+
+  let empty_line_of_code () = printf "\n<br/>\n"
+
+  let char = function
+    | '<' -> printf "&lt;"
+    | '>' -> printf "&gt;"
+    | '&' -> printf "&amp;"
+    | c -> output_char c
+
+  let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done
+
+  let latex_char _ = ()
+  let latex_string _ = ()
+
+  let html_char = output_char
+  let html_string = output_string
+
+  let start_latex_math () = ()
+  let stop_latex_math () = ()
+
+  let start_verbatim () = printf "<pre>"
+  let stop_verbatim () = printf "</pre>\n"
+
+  let module_ref m s = 
+    printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
+    (*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 s = match find_module m with
+    | Local ->
+	printf "<a href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
+    | Coqlib when !externals ->
+	let m = Filename.concat !coqlib m in
+	printf "<a href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
+    | Coqlib | Unknown ->
+	raw_ident s
+
+  let ident s loc = 
+    if is_keyword s then begin
+      printf "<code class=\"keyword\">"; 
+      raw_ident s; 
+      printf "</code>"
+    end else 
+      try
+	(match Index.find !current_module loc with
+	   | Def _ -> 
+	       printf "<a name=\"%s\"></a>" s; raw_ident s
+           | Mod (m,s') when s = s' ->
+	       module_ref m s
+	   | Ref (m,s') when s = s' -> 
+	       ident_ref m s
+	   | Mod _ | Ref _ ->
+	       raw_ident s)
+      with Not_found ->
+	raw_ident s
+	  
+  let with_html_printing f tok =
+    try 
+      (match Hashtbl.find token_pp tok with
+	 | _, Some s -> output_string s
+	 | _ -> f tok)
+    with Not_found -> 
+      f tok
+
+  let ident s l = with_html_printing (fun s -> ident s l) s
+
+  let symbol = with_html_printing raw_ident
+
+  let rec reach_item_level n = 
+    if !item_level < n then begin
+      printf "\n<ul>\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;
+      reach_item_level n
+    end
+
+  let item n =
+    let old_level = !item_level in
+    reach_item_level n;
+    if n <= old_level then printf "\n</li>\n<li>"
+
+  let stop_item () = reach_item_level 0
+
+  let start_coq () = if not !raw_comments then printf "<code>\n"
+
+  let end_coq () = if not !raw_comments then printf "</code>\n"
+
+  let start_doc () = 
+    if not !raw_comments then
+      printf "\n<table width=\"100%%\"><tr class=\"doc\"><td>\n"
+
+  let end_doc () =
+    stop_item (); 
+    if not !raw_comments then printf "\n</td></tr></table>\n"
+
+  let start_code () = end_doc (); start_coq ()
+
+  let end_code () = end_coq (); start_doc ()
+
+  let start_inline_coq () = printf "<code>"
+
+  let end_inline_coq () = printf "</code>"
+
+  let paragraph () = stop_item (); printf "\n<br/><br/>\n"
+
+  let section lev f =
+    let lab = new_label () in
+    let r = sprintf "%s.html#%s" !current_module lab in
+    add_toc_entry (Toc_section (lev, f, r));
+    stop_item ();
+    printf "<a name=\"%s\"></a><h%d>" lab lev;
+    f ();
+    printf "</h%d>\n" lev
+
+  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
+    if !multi_index then "index_" ^ idxc ^ ".html" else "index.html#" ^ idxc
+
+  let letter_index category idx (c,l) =
+    if l <> [] then begin
+      let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in
+      printf "<a name=\"%s_%c\"></a><h2>%c %s</h2>\n" idx c c cat;
+      List.iter 
+	(fun (id,(text,link)) -> 
+	   printf "<a href=\"%s\">%s</a> %s<br/>\n" link id text) l;
+      printf "<br/><br/>"
+    end
+		
+  let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries
+
+  let separate_index navig i =
+    let idx = i.idx_name in
+    let one_letter ((c,l) as cl) =
+      set_out_file (sprintf "index_%s_%c.html" idx c);
+      header ();
+      navig ();
+      printf "<hr/>";
+      letter_index true idx cl;
+      if List.length l > 30 then begin printf "<hr/>"; navig () end;
+      trailer ();
+      close ()
+    in
+    List.iter one_letter i.idx_entries
+
+  let format_global_index =
+    Index.map 
+      (fun s (m,t) -> 
+	 if t = Library then 
+	   "[library]", m ^ ".html"
+	 else
+	   sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (entry_type t) m m ,
+	   sprintf "%s.html#%s" m s)
+
+  let format_bytype_index = function
+    | Library, idx ->
+	Index.map (fun id m -> "", m ^ ".html") idx
+    | (t,idx) ->
+	Index.map 
+	  (fun s m -> 
+	     let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in
+	     (text, sprintf "%s.html#%s" m s)) idx
+
+  let navig_one_index i =
+    printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name);
+    List.iter 
+      (fun (c,l) -> 
+	 if l <> [] then
+	   printf "<td><a href=\"%s\">%c</a></td>\n" (index_ref i c) c
+	 else
+	   printf "<td>%c</td>\n" c)
+      i.idx_entries;
+    let n = i.idx_size in
+    printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry");
+    printf "</tr>\n"
+
+  let navig_index il = 
+    printf "<table>\n";
+    List.iter navig_one_index il;
+    printf "</table>\n"
+
+  let make_index () =
+    if !index then begin
+      let idxl = 
+	let glob,bt = Index.all_entries () in
+	format_global_index glob ::
+	List.map format_bytype_index bt 
+      in
+      let navig () = navig_index idxl in 
+      set_out_file "index.html";
+      current_module := "Index";
+      page_title := (if !title <> "" then !title else "Index");
+      header ();
+      if !title <> "" then printf "<h1>%s</h1>\n" !title;
+      navig ();
+      if !multi_index then begin
+	trailer (); 
+	close ();
+	List.iter (separate_index navig) idxl;
+      end else begin
+	let one_index i =
+	  if i.idx_size > 0 then begin
+	    printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
+	    all_letters i
+	  end
+	in
+	List.iter one_index idxl;
+	printf "<hr/>";
+	navig ();
+	trailer ();
+	close ()
+      end;
+    end
+
+  let make_toc () = 
+    set_out_file "toc.html";
+    page_title := (if !title <> "" then !title else "Table of contents");
+    header ();
+    if !title <> "" then printf "<h1>%s</h1>\n" !title;
+    let make_toc_entry = function
+      | Toc_library m -> 
+	  stop_item ();
+	  printf "<a href=\"%s.html\"><h2>Library %s</h2></a>\n" m m
+      | Toc_section (n, f, r) ->
+	  item n; 
+	  printf "<a href=\"%s\">" r; f (); printf "</a>\n"
+    in
+    Queue.iter make_toc_entry toc_q;
+    stop_item ();
+    if !index then printf "<a href=\"index.html\"><h2>Index</h2></a>";
+    trailer ();
+    close ()
+
+end
+
+
+(*s TeXmacs-aware output *)
+
+module TeXmacs = struct
+
+  (*s Latex preamble *)
+
+  let in_doc = ref false
+
+  let (preamble : string Queue.t) = 
+    in_doc := false; Queue.create ()
+
+  let push_in_preamble s = Queue.add s preamble
+
+  let header () =
+    output_string 
+      "(*i This file has been automatically generated with the command  \n";
+    output_string 
+      "    "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf " *)\n"
+
+  let trailer () = ()
+
+  let char_true c = match c with
+    | '\\' -> printf "\\\\"
+    | '<' -> printf "\\<"
+    | '|' -> printf "\\|"
+    | '>' -> printf "\\>"
+    | _ -> output_char c
+
+  let char c = if !in_doc then char_true c else output_char c
+
+  let latex_char = char_true
+  let latex_string = String.iter latex_char
+
+  let html_char _ = ()
+  let html_string _ = ()
+
+  let raw_ident s =
+    for i = 0 to String.length s - 1 do char s.[i] done
+
+  let start_module () = ()
+
+  let start_latex_math () = printf "<with|mode|math|"
+
+  let stop_latex_math () = output_char '>'
+
+  let start_verbatim () = in_doc := true; printf "<\\verbatim>"
+
+  let stop_verbatim () = in_doc := false; printf "</verbatim>"
+
+  let indentation n = ()
+
+  let ident_true s = 
+    if is_keyword s then begin
+      printf "<kw|"; raw_ident s; printf ">"
+    end else begin
+      raw_ident s
+    end
+
+  let ident s _ = if !in_doc then ident_true s else raw_ident s
+ 
+  let symbol_true s = 
+    let ensuremath x = printf "<with|mode|math|\\<%s\\>>" x in
+      match s with
+	| "*"  -> ensuremath "times"
+	| "->" -> ensuremath "rightarrow"
+	| "<-" -> ensuremath "leftarrow"
+	| "<->" ->ensuremath "leftrightarrow"
+	| "=>" -> ensuremath "Rightarrow"
+	| "<=" -> ensuremath "le"
+	| ">=" -> ensuremath "ge"
+	| "<>" -> ensuremath "noteq"
+	| "~" ->  ensuremath "lnot"
+	| "/\\" -> ensuremath "land"
+	| "\\/" -> ensuremath "lor"
+	| "|-" -> ensuremath "vdash"
+	| s    -> raw_ident s
+
+  let symbol s = if !in_doc then symbol_true s else raw_ident s
+
+  let rec reach_item_level n = 
+    if !item_level < n then begin
+      printf "\n<\\itemize>\n<item>"; incr item_level;
+      reach_item_level n
+    end else if !item_level > n then begin
+      printf "\n</itemize>"; decr item_level;
+      reach_item_level n
+    end
+
+  let item n =
+    let old_level = !item_level in
+    reach_item_level n;
+    if n <= old_level then printf "\n\n<item>"
+
+  let stop_item () = reach_item_level 0
+
+  let start_doc () = in_doc := true; printf "(** texmacs: "
+
+  let end_doc () = stop_item (); in_doc := false; printf " *)"
+
+  let start_coq () = ()
+
+  let end_coq () = ()
+
+  let start_code () = in_doc := true; printf "<\\code>\n"
+  let end_code () = in_doc := false; printf "\n</code>"
+
+  let section_kind = function
+    | 1 -> "section"
+    | 2 -> "subsection"
+    | 3 -> "subsubsection"
+    | 4 -> "paragraph"
+    | _ -> assert false
+
+  let section lev f =
+    stop_item ();
+    printf "<"; output_string (section_kind lev); printf "|"; 
+    f (); printf ">\n\n"
+
+  let rule () =
+    printf "\n<hrule>\n"
+
+  let paragraph () = stop_item (); printf "\n\n"
+
+  let line_break_true () = printf "<format|line break>"
+
+  let line_break () = printf "\n"
+
+  let empty_line_of_code () = printf "\n"
+
+  let start_inline_coq () = printf "<verbatim|["
+
+  let end_inline_coq () = printf "]>"
+
+  let make_index () = ()
+
+  let make_toc () = ()
+
+end
+
+(*s Generic output *)
+
+let select f1 f2 f3 x = 
+  match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x
+
+let push_in_preamble = Latex.push_in_preamble
+
+let header = select Latex.header Html.header TeXmacs.header
+let trailer = select Latex.trailer Html.trailer TeXmacs.trailer
+
+let start_module = 
+  select Latex.start_module Html.start_module TeXmacs.start_module
+
+let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc
+let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc
+
+let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq
+let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq
+
+let start_code = select Latex.start_code Html.start_code TeXmacs.start_code
+let end_code = select Latex.end_code Html.end_code TeXmacs.end_code
+
+let start_inline_coq = 
+  select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq
+let end_inline_coq = 
+  select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq
+
+let indentation = select Latex.indentation Html.indentation TeXmacs.indentation
+let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph
+let line_break = select Latex.line_break Html.line_break TeXmacs.line_break
+let empty_line_of_code = select 
+  Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code
+
+let section = select Latex.section Html.section TeXmacs.section
+let item = select Latex.item Html.item TeXmacs.item
+let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item
+let rule = select Latex.rule Html.rule TeXmacs.rule
+
+let char = select Latex.char Html.char TeXmacs.char
+let ident = select Latex.ident Html.ident TeXmacs.ident
+let symbol = select Latex.symbol Html.symbol TeXmacs.symbol
+
+let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char
+let latex_string = 
+  select Latex.latex_string Html.latex_string TeXmacs.latex_string
+let html_char = select Latex.html_char Html.html_char TeXmacs.html_char
+let html_string = 
+  select Latex.html_string Html.html_string TeXmacs.html_string
+
+let start_latex_math = 
+  select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math
+let stop_latex_math = 
+  select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math
+
+let start_verbatim = 
+  select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim
+let stop_verbatim = 
+  select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim
+let verbatim_char = 
+  select output_char Html.char TeXmacs.char
+let hard_verbatim_char = output_char
+
+let make_index = select Latex.make_index Html.make_index TeXmacs.make_index
+let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
new file mode 100644
index 00000000..2195fa53
--- /dev/null
+++ b/tools/coqdoc/output.mli
@@ -0,0 +1,92 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: output.mli,v 1.3.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+
+open Index
+
+type target_language = LaTeX | HTML | TeXmacs
+
+val target_language : target_language ref
+
+val set_out_file : string -> unit
+val output_dir : string ref
+val close : unit -> unit
+
+val quiet : bool ref
+val short : bool ref
+val light : bool ref
+val header_trailer : bool ref
+val index : bool ref
+val multi_index : bool ref
+val toc : bool ref
+val title : string ref
+val externals : bool ref
+val coqlib : string ref
+val raw_comments : bool ref
+
+val charset : string ref
+val inputenc : string ref
+val set_latin1 : unit -> unit
+val set_utf8 : unit -> unit
+
+val add_printing_token : string -> string option * string option -> unit
+val remove_printing_token : string -> unit
+
+val set_module : coq_module -> unit
+
+val header : unit -> unit
+val trailer : unit -> unit
+
+val push_in_preamble : string -> unit
+
+val dump_file : string -> unit
+
+val start_module : unit -> unit
+
+val start_doc : unit -> unit
+val end_doc : unit -> unit
+
+val start_coq : unit -> unit
+val end_coq : unit -> unit
+
+val start_code : unit -> unit
+val end_code : unit -> unit
+
+val start_inline_coq : unit -> unit
+val end_inline_coq : unit -> unit
+
+val indentation : int -> unit
+val line_break : unit -> unit
+val paragraph : unit -> unit
+val empty_line_of_code : unit -> unit
+
+val section : int -> (unit -> unit) -> unit
+
+val item : int -> unit
+
+val rule : unit -> unit
+
+val char : char -> unit
+val ident : string -> loc -> unit
+val symbol : string -> unit
+
+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 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 make_index : unit -> unit
+val make_toc : unit -> unit
diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/pretty.mli
new file mode 100644
index 00000000..07808fe9
--- /dev/null
+++ b/tools/coqdoc/pretty.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: pretty.mli,v 1.1.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+
+open Index
+
+type file =
+  | Vernac_file of string * coq_module
+  | Latex_file of string
+
+val gallina : bool ref
+
+val produce_document : file list -> unit
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
new file mode 100644
index 00000000..541939b5
--- /dev/null
+++ b/tools/coqdoc/pretty.mll
@@ -0,0 +1,586 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: pretty.mll,v 1.7.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+
+(*s Utility functions for the scanners *)
+
+{
+
+  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
+	| '\t' -> count (c + (8 - (c mod 8))) (i + 1)
+	| ' ' -> count (c + 1) (i + 1)
+	| _ -> c
+    in
+    count 0 0
+
+  let count_dashes s =
+    let c = ref 0 in
+    for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done;
+    !c
+
+  let cut_head_tail_spaces s =
+    let n = String.length s in
+    let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in
+    let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in
+    let l = look_up 0 in
+    let r = look_dn (n-1) in
+    if l <= r then String.sub s l (r-l+1) else s
+
+  let sec_title s =
+    let rec count lev i = 
+      if s.[i] = '*' then 
+	count (succ lev) (succ i) 
+      else 
+	let t = String.sub s i (String.length s - i) in
+	lev, cut_head_tail_spaces t
+    in
+    count 0 (String.index s '*')
+
+  let formatted = ref false
+  let brackets = ref 0
+
+  let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
+
+  (* Gallina (skipping proofs). This is a three states automaton. *)   
+
+  let gallina = ref false
+
+  type gallina_state = Nothing | AfterDot | Proof
+
+  let gstate = ref AfterDot
+
+  let is_proof = 
+    let t = Hashtbl.create 13 in
+    List.iter (fun s -> Hashtbl.add t s true)
+      [ "Theorem"; "Lemma"; "Fact"; "Remark"; "Goal"; "Let";
+	"Correctness"; "Definition"; "Morphism" ];
+    fun s -> try Hashtbl.find t s with Not_found -> false
+
+  let gallina_id id = 
+    if !gstate = AfterDot then
+      if is_proof id then gstate := Proof else 
+	if id <> "Add" then gstate := Nothing
+
+  let gallina_symbol s = 
+    if !gstate = AfterDot || (!gstate = Proof && s = ":=") then 
+      gstate := Nothing
+
+  let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
+
+  let gallina_char c = 
+    if c = '.' then
+      (let skip = !gstate = Proof in gstate := AfterDot; skip)
+    else
+      (if !gstate = AfterDot && not (is_space c) then gstate := Nothing;
+       false)
+
+  (* saving/restoring the PP state *)
+
+  type state = {
+    st_gallina : bool;
+    st_light : bool
+  }
+
+  let state_stack = Stack.create ()
+
+  let save_state () = 
+    Stack.push { st_gallina = !gallina; st_light = !light } state_stack
+
+  let restore_state () =
+    let s = Stack.pop state_stack in
+    gallina := s.st_gallina;
+    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_light = without_ref light
+
+  let show_all f = without_gallina (without_light f)
+
+  let begin_show () = save_state (); gallina := false; light := false
+  let end_show () = restore_state ()
+
+  (* Reset the globals *)
+
+  let reset () =
+    formatted := false;
+    brackets := 0;
+    gstate := AfterDot
+
+  (* erasing of Section/End *)
+
+  let section_re = Str.regexp "[ \t]*Section"
+  let end_re = Str.regexp "[ \t]*End"
+  let is_section s = Str.string_match section_re s 0
+  let is_end s = Str.string_match end_re s 0
+
+  let sections_to_close = ref 0
+
+  let section_or_end s =
+    if is_section s then begin
+      incr sections_to_close; true
+    end else if is_end s then begin
+      if !sections_to_close > 0 then begin 
+	decr sections_to_close; true 
+      end else 
+	false
+    end else
+      true
+
+  (* tokens pretty-print *)
+
+  let token_buffer = Buffer.create 1024
+
+  let token_re = 
+    Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
+  let printing_token_re =
+    Str.regexp
+      "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?"
+
+  let add_printing_token toks pps =
+    try
+      if Str.string_match token_re toks 0 then
+	let tok = Str.matched_group 1 toks in
+	if Str.string_match printing_token_re pps 0 then
+	  let pp = 
+	    (try Some (Str.matched_group 3 pps) with _ -> 
+             try Some (Str.matched_group 4 pps) with _ -> None),
+	    (try Some (Str.matched_group 6 pps) with _ -> None)
+	  in
+	  Output.add_printing_token tok pp
+    with _ ->
+      ()
+
+  let remove_token_re = 
+    Str.regexp 
+      "[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)"
+
+  let remove_printing_token toks =
+    try
+      if Str.string_match remove_token_re toks 0 then
+	let tok = Str.matched_group 1 toks in
+	Output.remove_printing_token tok
+    with _ ->
+      ()
+
+  let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
+  let extract_ident s =
+    assert (String.length s >= 3);
+    if Str.string_match extract_ident_re s 0 then
+      Str.matched_group 1 s
+    else
+      String.sub s 1 (String.length s - 3)
+
+}
+
+(*s Regular expressions *)
+
+let space = [' ' '\t']
+let space_nl = [' ' '\t' '\n' '\r']
+
+let firstchar = 
+  ['A'-'Z' 'a'-'z' '_' 
+  (* iso 8859-1 accents *) 
+  '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+  (* utf-8 latin 1 supplement *) 
+  '\195' ['\128'-'\191'] |
+  (* utf-8 letterlike symbols *) 
+  '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+let identchar = 
+  firstchar | ['\'' '0'-'9' '@']
+let identifier = firstchar identchar*
+
+let symbolchar_no_brackets =
+  ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#'
+   '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~'
+   '{' '}' '(' ')'] |
+  (* utf-8 symbols *) 
+  '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
+let symbolchar = symbolchar_no_brackets | '[' | ']'
+let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
+
+(* tokens with balanced brackets *)
+let token_brackets =
+  ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* 
+  | symbolchar_no_brackets* ('[' symbolchar_no_brackets* ']')+ )
+  symbolchar_no_brackets*
+
+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_verb = "(*" space* "begin" space+ "verb" space* "*)"
+let end_verb = "(*" space* "end" space+ "verb" space* "*)"
+*)
+
+let coq_command_to_hide =
+  "Implicit" space |
+  "Ltac" space | 
+  "Require" space | 
+  "Load" space |
+  "Hint" space |
+  "Transparent" space |
+  "Opaque" space |
+  ("Declare" space+ ("Morphism" | "Step") space) |
+  "Section" space | 
+  "Variable" 's'? space | 
+  ("Hypothesis" | "Hypotheses") space | 
+  "End" space |
+  ("Set" | "Unset") space+ "Printing" space+ "Coercions" space |
+  "Declare" space+ ("Left" | "Right") space+ "Step" space
+
+(*s Scanning Coq, at beginning of line *)
+
+rule coq_bol = parse
+  | '\n'+
+      { empty_line_of_code (); coq_bol lexbuf }
+  | space* "(**" space_nl
+      { end_coq (); start_doc (); 
+	let eol = doc_bol lexbuf in
+	end_doc (); 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 }
+  | space* begin_hide
+      { skip_hide lexbuf; coq_bol lexbuf }
+  | space* begin_show
+      { begin_show (); coq_bol lexbuf }
+  | space* end_show
+      { end_show (); coq_bol lexbuf }
+  | space* coq_command_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
+	  indentation (count_spaces s); 
+	  backtrack lexbuf; 
+	  coq lexbuf 
+	end }
+  | space* "(**" space+ "printing" space+ (identifier | token) space+
+      { let tok = lexeme lexbuf in
+	let s = printing_token lexbuf in
+	add_printing_token tok s;
+	coq_bol lexbuf }
+  | space* "(**" space+ "printing" space+
+      { eprintf "warning: bad 'printing' command at character %d\n" 
+	  (lexeme_start lexbuf); flush stderr;
+	ignore (comment lexbuf);
+	coq_bol lexbuf }
+  | space* "(**" space+ "remove" space+ "printing" space+ 
+    (identifier | token) space* "*)"
+      { remove_printing_token (lexeme lexbuf);
+	coq_bol lexbuf }
+  | space* "(**" space+ "remove" space+ "printing" space+
+      { eprintf "warning: bad 'remove printing' command at character %d\n" 
+	  (lexeme_start lexbuf); flush stderr;
+	ignore (comment lexbuf);
+	coq_bol lexbuf }
+  | space* "(*"
+      { let eol = comment lexbuf in
+	if eol then coq_bol lexbuf else coq lexbuf }
+  | space+
+      { indentation (count_spaces (lexeme lexbuf)); coq lexbuf }
+  | eof 
+      { () }
+  | _ 
+      { backtrack lexbuf; indentation 0; coq lexbuf }
+
+(*s Scanning Coq elsewhere *)
+
+and coq = parse
+  | "\n" 
+      { line_break (); coq_bol lexbuf }
+  | "(**" space_nl
+      { end_coq (); start_doc (); 
+	let eol = doc_bol lexbuf in
+	end_doc (); start_coq (); 
+	if eol then coq_bol lexbuf else coq lexbuf }
+  | "(*"
+      { let eol = comment lexbuf in
+	if eol then coq_bol lexbuf else coq lexbuf }
+  | '\n'+ space* "]]"
+      { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end }
+  | eof 
+      { () }
+  | token
+      { let s = lexeme lexbuf in
+	if !gallina then gallina_symbol s;
+	symbol s;
+	coq lexbuf }
+  | "with" space+ "Module" | "Module" space+ "Type" | "Declare" space+ "Module"
+    (* hack to avoid making Type a keyword *)
+      { let s = lexeme lexbuf in
+	if !gallina then gallina_id s;
+        ident s (lexeme_start lexbuf); coq lexbuf }
+  | "(" space* identifier space* ":=" 
+      { let id = extract_ident (lexeme lexbuf) in
+	symbol "("; ident id (lexeme_start lexbuf); symbol ":="; coq lexbuf }
+  | (identifier '.')* identifier
+      { let id = lexeme lexbuf in
+	if !gallina then gallina_id id;
+	ident id (lexeme_start lexbuf); coq lexbuf }
+  | _ 
+      { let c = lexeme_char lexbuf 0 in 
+	char c;
+	if !gallina && gallina_char c then skip_proof lexbuf;
+	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 }
+  | eof 
+      { false }
+  | _ 
+      { backtrack lexbuf; doc lexbuf }
+
+(*s Scanning documentation elsewhere *)
+
+and doc = parse
+  | "\n"
+      { char '\n'; doc_bol lexbuf }
+  | "["
+      { brackets := 1; 
+	start_inline_coq (); escaped_coq lexbuf; end_inline_coq ();
+	doc lexbuf }
+  | "[[" '\n' space*
+      { formatted := true; start_code ();
+	indentation (count_spaces (lexeme lexbuf)); 
+	without_gallina coq lexbuf; 
+	end_code (); formatted := false;
+	doc lexbuf }
+  | '*'* "*)" space* '\n'
+      { true }
+  | '*'* "*)"
+      { false }
+  | "$"
+      { start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
+  | "$$"
+      { char '$'; doc lexbuf }
+  | "%"
+      { escaped_latex lexbuf; doc lexbuf }
+  | "%%"
+      { char '%'; doc lexbuf }
+  | "#"
+      { escaped_html lexbuf; doc lexbuf }
+  | "##"
+      { char '#'; doc lexbuf }
+  | eof 
+      { false }
+  | _ 
+      { 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 }
+
+and escaped_latex = parse
+  | "%" { () }
+  | eof { () }
+  | _   { latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
+
+and escaped_html = parse
+  | "#" { () }
+  | "&#"
+        { html_char '&'; html_char '#'; escaped_html lexbuf }
+  | "##"
+        { html_char '#'; escaped_html lexbuf }
+  | eof { () }
+  | _   { 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 }
+
+(*s Coq, inside quotations *)
+
+and escaped_coq = parse
+  | "]"
+      { decr brackets; 
+	if !brackets > 0 then begin char ']'; escaped_coq lexbuf end }
+  | "["
+      { incr brackets; char '['; escaped_coq lexbuf }
+  | "(*"
+      { ignore (comment lexbuf); escaped_coq lexbuf }
+  | "*)"
+      { (* likely to be a syntax error: we escape *) backtrack lexbuf }
+  | eof
+      { () }
+  | token_brackets
+      { let s = lexeme lexbuf in
+	symbol s;
+	escaped_coq lexbuf }
+  | (identifier '.')* identifier
+      { ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
+  | _ 
+      { char (lexeme_char lexbuf 0); escaped_coq lexbuf }
+
+(*s Coq "Comments" command. *)
+
+and comments = parse
+  | space_nl+ 
+      { char ' '; comments lexbuf }
+  | '"' [^ '"']* '"' 
+      { let s = lexeme lexbuf in
+	let s = String.sub s 1 (String.length s - 2) in
+	ignore (doc (from_string s)); comments lexbuf }
+  | ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+
+      { escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
+  | "." (space_nl | eof)
+      { () }
+  | eof 
+      { () }
+  | _   
+      { char (lexeme_char lexbuf 0); comments lexbuf }
+
+(*s Skip comments *)
+
+and comment = parse
+  | "(*" { ignore (comment lexbuf); comment lexbuf }
+  | "*)" space* '\n'+ { true }
+  | "*)" { false }
+  | eof  { false }
+  | _    { comment lexbuf }
+
+(*s Skip proofs *)
+
+and skip_proof = parse
+  | "(*" { ignore (comment lexbuf); skip_proof lexbuf }
+  | "Save" | "Qed" | "Defined"
+  | "Abort" | "Proof" | "Admitted" { skip_to_dot lexbuf }
+  | "Proof" space* '.' { skip_proof lexbuf }
+  | identifier { skip_proof lexbuf } (* to avoid keywords within idents *)
+  | eof { () }
+  | _ { skip_proof lexbuf }
+
+and skip_to_dot = parse
+  | eof | '.' { if !gallina then gstate := AfterDot }
+  | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
+  | _ { skip_to_dot lexbuf }
+
+and skip_hide = parse
+  | eof | end_hide { () }
+  | _ { skip_hide lexbuf }
+
+(*s Reading token pretty-print *)
+
+and printing_token = parse
+  | "*)" | eof 
+	{ let s = Buffer.contents token_buffer in 
+	  Buffer.clear token_buffer;
+	  s }
+  | _   { Buffer.add_string token_buffer (lexeme lexbuf); 
+	  printing_token lexbuf }
+
+(*s Applying the scanners to files *)
+
+{
+
+  type file =
+    | Vernac_file of string * coq_module
+    | Latex_file of string
+
+  let coq_file f m =
+    reset ();
+    Index.scan_file f m;
+    start_module ();
+    let c = open_in f in
+    let lb = from_channel c in
+    start_coq (); coq_bol lb; end_coq ();
+    close_in c
+
+  (* LaTeX document *)
+
+  let latex_document l = 
+    let file = function
+      | Vernac_file (f,m) -> set_module m; coq_file f m
+      | Latex_file f -> dump_file f
+    in
+    header ();
+    if !toc then make_toc ();
+    List.iter file l;
+    trailer ();
+    close ()
+
+  (* HTML document *)      
+
+  let html_document l =
+    let file = function
+      | Vernac_file (f,m) -> 
+	  set_module m;
+	  let hf = m ^ ".html" in
+	  set_out_file hf;
+	  header ();
+	  coq_file f m;
+	  trailer ();
+	  close ()
+      | Latex_file _ -> ()
+    in
+    List.iter file l;
+    make_index ();
+    if !toc then make_toc ()
+
+  (* TeXmacs document *)
+
+  let texmacs_document l = 
+    let file = function
+      | Vernac_file (f,m) -> set_module m; coq_file f m
+      | Latex_file f -> dump_file f
+    in
+    header ();
+    List.iter file l;
+    trailer ();
+    close ()
+
+  let index_module = function
+    | Vernac_file (_,m) -> Index.add_module m
+    | Latex_file _ -> ()
+
+  let produce_document l =
+    List.iter index_module l;
+    (match !target_language with
+       | LaTeX -> latex_document 
+       | HTML -> html_document
+       | TeXmacs -> texmacs_document) l
+
+}
+
diff --git a/tools/coqdoc/style.css b/tools/coqdoc/style.css
new file mode 100644
index 00000000..5150bd75
--- /dev/null
+++ b/tools/coqdoc/style.css
@@ -0,0 +1,23 @@
+a:visited {color : #416DFF; text-decoration : none; }
+a:link {color : #416DFF; text-decoration : none; font-weight : bold}
+a:hover {color : Red; text-decoration : underline; }
+a:active {color : Red; text-decoration : underline; }
+.keyword { font-weight : bold ; color : Red }
+.keywordsign { color : #C04600 }
+.superscript { font-size : 4 }
+.subscript { font-size : 4 }
+.comment { color : Green }
+.constructor { color : Blue }
+.string { color : Maroon }
+.warning { color : Red ; font-weight : bold }
+.info { margin-left : 3em; margin-right : 3em }
+.title1 { font-size : 20pt ; background-color : #416DFF }
+.title2 { font-size : 20pt ; background-color : #418DFF }
+.title3 { font-size : 20pt ; background-color : #41ADFF }
+.title4 { font-size : 20pt ; background-color : #41CDFF }
+.title5 { font-size : 20pt ; background-color : #41EDFF }
+.title6 { font-size : 20pt ; background-color : #41FFFF }
+body { background-color : White }
+tr { background-color : White }
+# .doc { background-color :#aaeeff  }
+.doc { background-color :#66ff66  }