Several bug-fixes and improvements of coqdoc

- make links to section variables working (used qualified names for
  disambiguation and fixed the place in intern_var where to dump them)
  (wish #2277)
- mapping of physical to logical paths now follows coq (see bug #2274)
  (incidentally, it was also incorrectly seeing foobar.v as a in directory foo)
- added links for notations
- added new category "other" for indexing entries not starting with latin letter
  (e.g. notations or non-latin identifiers which was otherwise broken)
- protected non-notation strings (from String.v) from utf8 symbol interpretation
- incidentally quoted parseable _ in notations to avoid confusion with
  placeholder in the "_ + _" form of notation
- improved several "Sys_error" error messages
- fixed old bug about second dot of ".." being interpreted as regular dot
- removed obsolete lexer in index.mll (and renamed index.mll to index.ml)
- added a test-suite file for testing various features of coqdoc

Things that still do not work:
- when a notation is redefined several times in the same scope, only
  the link to the first definition works
- if chars and symbols are not separated in advance, idents
  that immediately follow symbols are not detected
  (e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}")
- parentheses, curly brackets and semi-colon not linked in notations

Things that can probably be improved:
- all notations are indexed in the same category "other"; can we do better?
- all non-latin identifiers (e.g. Greek letters) are also indexed in the
  same "other" category; can we do better?
- globalization data for notations could be compacted (currently there is one
  line per each proper location covered by the notation)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 513 insertions, 639 deletions

diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index fe26e0086c..d25034f2a3 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -8,7 +8,9 @@
 
 (*i $Id$ i*)
 
-let norm_char c = match Char.uppercase c with
+open Cdglobals
+
+let norm_char_latin1 c = match Char.uppercase c with
   | '\192'..'\198' -> 'A'
   | '\199' -> 'C'
   | '\200'..'\203' -> 'E'
@@ -19,6 +21,13 @@ let norm_char c = match Char.uppercase c with
   | '\221' -> 'Y'
   | c -> c
 
+let norm_char_utf8 c = Char.uppercase c
+
+let norm_char c =
+  if !utf8 then norm_char_utf8 c else
+  if !latin1 then norm_char_latin1 c else
+  Char.uppercase c
+
 let norm_string s =
   let u = String.copy s in
   for i = 0 to String.length s - 1 do
@@ -30,6 +39,8 @@ 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
+  | '_', _ -> -1
+  | _, '_' -> 1
   | c1, c2 -> compare c1 c2
 
 let compare_string s1 s2 =
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 4994a12803..b2e23657b1 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -25,9 +25,19 @@ let out_to = ref MultFiles
 
 let out_channel = ref stdout
 
+let coqdoc_out f =
+  if !output_dir <> "" && Filename.is_relative f then
+    if not (Sys.file_exists !output_dir) then
+      (Printf.eprintf "No such directory: %s\n" !output_dir; exit 1)
+    else
+      Filename.concat !output_dir f
+  else
+    f
+
 let open_out_file f =
-  let f = if !output_dir <> "" && Filename.is_relative f then Filename.concat !output_dir f else f in
-    out_channel := open_out f
+  out_channel :=
+    try open_out (coqdoc_out f)
+    with Sys_error s -> Printf.eprintf "%s\n" s; exit 1
 
 let close_out_file () = close_out !out_channel
 
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 071b3d5558..97d581048a 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -247,7 +247,13 @@
     else
       String.sub s 1 (String.length s - 3)
 
-  let symbol lexbuf s = Output.symbol s
+  let symbol lexbuf s = Output.symbol s (lexeme_start lexbuf)
+
+  let output_indented_keyword s lexbuf =
+    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)
 
 }
 
@@ -359,16 +365,18 @@ let gallina_ext =
   | "Coercion"
   | "Identity"
   | "Implicit"
-  | "Notation"
-  | "Infix"
   | "Tactic" space+ "Notation"
-  | "Reserved" space+ "Notation"
   | "Section"
   | "Context"
   | "Variable" 's'?
   | ("Hypothesis" | "Hypotheses")
   | "End"
 
+let notation_kw =
+    "Notation"
+  | "Infix"
+  | "Reserved" space+ "Notation"
+
 let commands =
   "Pwd"
   | "Cd"
@@ -439,8 +447,6 @@ let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
 let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 *)
 
-
-
 (*s Scanning Coq, at beginning of line *)
 
 rule coq_bol = parse
@@ -469,22 +475,16 @@ rule coq_bol = parse
 	      if eol then (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
+	      output_indented_keyword s lexbuf;
+	      let eol = body lexbuf in
+	      if eol then coq_bol lexbuf else coq lexbuf
 	    end }
   | space* thm_token
       { let s = lexeme lexbuf in
-	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
-	    in_proof := Some eol;
-	    if eol then coq_bol lexbuf else coq lexbuf }
+        output_indented_keyword s lexbuf;
+        let eol = body lexbuf in
+	in_proof := Some eol;
+	if eol then coq_bol lexbuf else coq lexbuf }
   | space* prf_token
       { in_proof := Some true;
 	let eol =
@@ -507,22 +507,21 @@ rule coq_bol = parse
       {
 	in_proof := None;
 	let s = lexeme lexbuf in
-	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 }
+	output_indented_keyword s lexbuf;
+	let eol= body lexbuf in
+	if eol then coq_bol lexbuf else coq lexbuf }
   | space* prog_kw
       {
 	in_proof := None;
 	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 }
+	output_indented_keyword s lexbuf;
+	let eol= body lexbuf in
+	if eol then coq_bol lexbuf else coq lexbuf }
+  | space* notation_kw space*
+      {	let s = lexeme lexbuf in
+	output_indented_keyword s lexbuf;
+	let eol= start_notation_string lexbuf in
+	if eol then coq_bol lexbuf else coq lexbuf }
 
   | space* "(**" space+ "printing" space+ printing_token space+
       { let tok = lexeme lexbuf in
@@ -634,6 +633,11 @@ and coq = parse
 	  Output.ident s (lexeme_start lexbuf);
 	let eol = body lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
+  | notation_kw space*
+      { let s = lexeme lexbuf in
+	Output.ident s (lexeme_start lexbuf);
+	let eol= start_notation_string lexbuf in
+	if eol then coq_bol lexbuf else coq lexbuf }
   | prog_kw
       { let s = lexeme lexbuf in
 	  Output.ident s (lexeme_start lexbuf);
@@ -1040,7 +1044,6 @@ and body = parse
       }
   | '.' space+ { Output.char '.'; Output.char ' ';
 	  if not !formatted then false else body lexbuf }
-  | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
   | "(**" space_nl
       { Output.end_coq (); Output.start_doc ();
 	let eol = doc_bol lexbuf in
@@ -1052,6 +1055,10 @@ and body = parse
 	     if eol
 	     then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
 	     else body lexbuf }
+  | "where" space*
+      { let s = lexeme lexbuf in
+	Output.ident s (lexeme_start lexbuf);
+	start_notation_string lexbuf }
   | identifier
       { let s = lexeme lexbuf in
 	  Output.ident s (lexeme_start lexbuf);
@@ -1059,24 +1066,34 @@ and body = parse
   | token_no_brackets
       { let s = lexeme lexbuf in
 	  symbol lexbuf s; body lexbuf }
+  | ".."
+      { Output.char '.'; Output.char '.';
+        body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in
 	  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 '"'}
+and start_notation_string = parse
+  | '"' (* a true notation *)
+      { symbol lexbuf "\"";
+        notation_string lexbuf;
+	body lexbuf }
+  | _ (* an abbreviation *)
+      { body lexbuf }
+
+and notation_string = parse
+  | "\"\""
+      { Output.char '"'; Output.char '"'; (* Unlikely! *)
+        notation_string lexbuf }
+  | '"'
+      { Output.char '"' }
   | token
       { let s = lexeme lexbuf in
-	  symbol lexbuf s; notation lexbuf }
+        symbol lexbuf s;
+        notation_string lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in
-	  Output.char c;
-          notation lexbuf }
+        Output.char c;
+        notation_string lexbuf }
 
 and skip_hide = parse
   | eof | end_hide { () }
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
new file mode 100644
index 0000000000..434a8bf5b5
--- /dev/null
+++ b/tools/coqdoc/index.ml
@@ -0,0 +1,328 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
+(************************************************************************)
+(*  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$ i*)
+
+open Filename
+open Lexing
+open Printf
+open Cdglobals
+
+type loc = int
+
+type entry_type =
+  | Library
+  | Module
+  | Definition
+  | 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 * entry_type
+  | Mod of coq_module * string
+
+let current_type : entry_type ref = ref Library
+let current_library = ref ""
+  (** refers to the file being parsed *)
+
+(** [deftable] stores only definitions and is used to interpolate idents
+    inside comments, which are not globalized otherwise. *)
+
+let deftable = Hashtbl.create 97
+
+(** [reftable] stores references and definitions *)
+let reftable = Hashtbl.create 97
+
+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 reftable (!current_library, loc) (Def (full_ident sp id, ty));
+  Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
+
+let add_ref m loc m' sp id ty =
+  if Hashtbl.mem reftable (m, loc) then ()
+  else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
+  let idx = if id = "<>" then m' else id in
+    if Hashtbl.mem deftable idx then ()
+    else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
+
+let add_mod m loc m' id =
+  Hashtbl.add reftable (m, loc) (Mod (m', id));
+  Hashtbl.add deftable m (Mod (m', id))
+
+let find m l = Hashtbl.find reftable (m, l)
+
+let find_string m s = Hashtbl.find deftable s
+
+(*s Manipulating path prefixes *)
+
+type stack = string list
+
+let rec string_of_stack st =
+  match st with
+    | [] -> ""
+    | x::[] -> x
+    | x::tl -> (string_of_stack tl) ^ "." ^ x
+
+let empty_stack = []
+
+let module_stack = ref empty_stack
+let section_stack = ref empty_stack
+
+let init_stack () =
+  module_stack := empty_stack; section_stack := empty_stack
+
+let push st p = st := p::!st
+let pop st =
+  match !st with
+    | [] -> ()
+    | _::tl -> st := tl
+
+let head st =
+  match st with
+    | [] -> ""
+    | x::_ -> x
+
+let begin_module m = push module_stack m
+let begin_section s = push section_stack s
+
+let end_block id =
+  (** determines if it ends a module or a section and pops the stack *)
+  if ((String.compare (head !module_stack) id ) == 0) then
+    pop module_stack
+  else if ((String.compare (head !section_stack) id) == 0) then
+    pop section_stack
+  else
+    ()
+
+let make_fullid id =
+  (** prepends the current module path to an id *)
+  let path = string_of_stack !module_stack in
+    if String.length path > 0 then
+      path ^ "." ^ 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
+
+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 | External of string | Unknown
+
+let external_libraries = ref []
+
+let add_external_library logicalpath url =
+  external_libraries := (logicalpath,url) :: !external_libraries
+
+let find_external_library logicalpath =
+  let rec aux = function
+    | [] -> raise Not_found
+    | (l,u)::rest ->
+        if String.length logicalpath > String.length l &
+          String.sub logicalpath 0 (String.length l + 1) = l ^"."
+        then u
+        else aux rest
+  in aux !external_libraries
+
+let init_coqlib_library () = add_external_library "Coq" !coqlib
+
+let find_module m =
+  if Hashtbl.mem local_modules m then
+    Local
+  else
+    try External (Filename.concat (find_external_library m) m)
+    with Not_found -> Unknown
+
+
+(* 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 c,l =
+	try c,Hashtbl.find t c with Not_found -> '*',Hashtbl.find t '*' 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 display_letter c = if c = '*' then "other" else String.make 1 c
+
+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 ->
+      let ln = !lib_name in
+        if ln <> "" then String.lowercase ln else "library"
+  | Module -> "moduleid"
+  | Definition -> "definition"
+  | 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 prepare_entry s = function
+  | Notation ->
+      (* Notations have conventially the form section.:sc:x_++_'x'_x *)
+      let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in
+      let h = try String.index_from s 0 ':' with _ -> err () in
+      let i = try String.index_from s (h+1) ':' with _ -> err () in
+      let sc = String.sub s (h+1) (i-h-1) in
+      let ntn = String.make (String.length s) ' ' in
+      let k = ref 0 in
+      let j = ref (i+1) in
+      let quoted = ref false in
+      while !j <> String.length s do
+	if s.[!j] = '_' && not !quoted then ntn.[!k] <- ' ' else
+	if s.[!j] = 'x' && not !quoted then ntn.[!k] <- '_' else
+	if s.[!j] = '\'' then
+	  if s.[!j+1] = 'x' && s.[!j+1] = '\'' then (ntn.[!k] <- 'x'; j:=!j+2)
+	  else (quoted := not !quoted; ntn.[!k] <- '\'')
+	else ntn.[!k] <- s.[!j];
+	incr j; incr k
+      done;
+      let ntn = String.sub ntn 0 !k in
+      if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
+  | _ ->
+      s
+
+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 reftable;
+    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 []
+
+let type_of_string = function
+  | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
+  | "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
+  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);
+	      current_library := !cur_mod
+	  | 'R' ->
+	      (try
+		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; assert false
+  with End_of_file ->
+    close_in c
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 3649d6a4a2..517ec97a75 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -52,13 +52,9 @@ val init_coqlib_library : unit -> unit
 
 val add_external_library : string -> coq_module -> unit
 
-(*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 -> coq_module
+val read_glob : string -> unit
 
 (*s Indexes *)
 
@@ -69,6 +65,10 @@ type 'a index = {
 
 val current_library : string ref
 
+val display_letter : char -> string
+
+val prepare_entry : string -> entry_type -> string
+
 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
deleted file mode 100644
index fe3b946e52..0000000000
--- a/tools/coqdoc/index.mll
+++ /dev/null
@@ -1,506 +0,0 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
-(************************************************************************)
-(*  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$ i*)
-
-{
-
-open Filename
-open Lexing
-open Printf
-
-open Cdglobals
-
-type loc = int
-
-type entry_type =
-  | Library
-  | Module
-  | Definition
-  | 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 * entry_type
-  | Mod of coq_module * string
-
-let current_type : entry_type ref = ref Library
-let current_library = ref ""
-  (** refers to the file being parsed *)
-
-(** [deftable] stores only definitions and is used to interpolate idents
-    inside comments, which are not globalized otherwise. *)
-
-let deftable = Hashtbl.create 97
-
-(** [reftable] stores references and definitions *)
-let reftable = Hashtbl.create 97
-
-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 reftable (!current_library, loc) (Def (full_ident sp id, ty));
-  Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
-
-let add_ref m loc m' sp id ty =
-  if Hashtbl.mem reftable (m, loc) then ()
-  else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
-  let idx = if id = "<>" then m' else id in
-    if Hashtbl.mem deftable idx then ()
-    else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
-
-let add_mod m loc m' id =
-  Hashtbl.add reftable (m, loc) (Mod (m', id));
-  Hashtbl.add deftable m (Mod (m', id))
-
-let find m l = Hashtbl.find reftable (m, l)
-
-let find_string m s = Hashtbl.find deftable s
-
-(*s Manipulating path prefixes *)
-
-type stack = string list
-
-let rec string_of_stack st =
-  match st with
-    | [] -> ""
-    | x::[] -> x
-    | x::tl -> (string_of_stack tl) ^ "." ^ x
-
-let empty_stack = []
-
-let module_stack = ref empty_stack
-let section_stack = ref empty_stack
-
-let init_stack () =
-  module_stack := empty_stack; section_stack := empty_stack
-
-let push st p = st := p::!st
-let pop st =
-  match !st with
-    | [] -> ()
-    | _::tl -> st := tl
-
-let head st =
-  match st with
-    | [] -> ""
-    | x::_ -> x
-
-let begin_module m = push module_stack m
-let begin_section s = push section_stack s
-
-let end_block id =
-  (** determines if it ends a module or a section and pops the stack *)
-  if ((String.compare (head !module_stack) id ) == 0) then
-    pop module_stack
-  else if ((String.compare (head !section_stack) id) == 0) then
-    pop section_stack
-  else
-    ()
-
-let make_fullid id =
-  (** prepends the current module path to an id *)
-  let path = string_of_stack !module_stack in
-    if String.length path > 0 then
-      path ^ "." ^ 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
-
-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 | External of string | Unknown
-
-let external_libraries = ref []
-
-let add_external_library logicalpath url =
-  external_libraries := (logicalpath,url) :: !external_libraries
-
-let find_external_library logicalpath =
-  let rec aux = function
-    | [] -> raise Not_found
-    | (l,u)::rest ->
-        if String.length logicalpath > String.length l &
-          String.sub logicalpath 0 (String.length l + 1) = l ^"."
-        then u
-        else aux rest
-  in aux !external_libraries
-
-let init_coqlib_library () = add_external_library "Coq" !coqlib
-
-let find_module m =
-  if Hashtbl.mem local_modules m then
-    Local
-  else
-    try External (Filename.concat (find_external_library m) m)
-    with Not_found -> Unknown
-
-
-(* 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 ->
-      let ln = !lib_name in
-        if ln <> "" then String.lowercase ln else "library"
-  | Module -> "moduleid"
-  | Definition -> "definition"
-  | 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
-  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 reftable;
-    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 digit = ['0'-'9']
-let num = digit+
-
-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 id = firstchar identchar*
-let pfx_id = (id '.')*
-let ident = id | pfx_id id
-
-let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
-let end_hide = "(*" space* "end" space+ "hide" space* "*)"
-
-(*s Indexing entry point. *)
-
-rule traverse = parse
-  | ("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 }
-  | ("Program" space+)? "Fixpoint" space
-      { current_type := Definition; index_ident lexbuf; fixpoint lexbuf;
-	traverse lexbuf }
-  | ("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;
-	index_ident lexbuf; inductive lexbuf; traverse lexbuf }
-  | "Record" space
-      { current_type := Inductive; index_ident lexbuf; traverse lexbuf }
-  | "Module" (space+ "Type")? space
-      { current_type := Module; module_ident lexbuf; traverse lexbuf }
-(*i***
-  | "Variable" 's'? space
-      { current_type := Variable; index_idents lexbuf; traverse lexbuf }
-***i*)
-  | "Require" (space+ ("Export"|"Import"))?
-      { module_refs lexbuf; traverse lexbuf }
-  | "End" space+
-      { end_ident 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
-      { let fullid =
-	  let id = lexeme lexbuf in
-	    match !current_type with
-	      | Definition
-	      | Inductive
-	      | Constructor
-	      | Lemma -> make_fullid id
-	      | _ -> id
-	in
-	  add_def (lexeme_start lexbuf) !current_type "" fullid }
-  | 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 }
-
-and end_ident = parse
-  | space+
-      { end_ident lexbuf }
-  | ident
-      { let id = lexeme lexbuf in end_block id }
-  | eof
-      { () }
-  | _
-      { () }
-
-and module_ident = parse
-  | space+
-      { module_ident lexbuf }
-  | '"' { string lexbuf; module_ident lexbuf }
-  | ident space* ":="
-      { () }
-  | ident
-      { let id = lexeme lexbuf in
-	  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" | "fix" | "cofix"
-    | "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
-    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);
-		current_library := !cur_mod
-	    | 'R' ->
-		(try
-		    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; assert false
-    with End_of_file ->
-      close_in c; !cur_mod
-
-  let scan_file f m =
-    init_stack (); current_library := 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
index 7fb9322d77..fb9b64b4fb 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -102,7 +102,7 @@ let target_full_name f =
 
 let check_if_file_exists f =
   if not (Sys.file_exists f) then begin
-    eprintf "\ncoqdoc: %s: no such file\n" f;
+    eprintf "coqdoc: %s: no such file\n" f;
     exit 1
   end
 
@@ -116,50 +116,44 @@ let normalize_path p =
      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
+  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
+  normalize_path dirname, basename
 
 (* [paths] maps a physical path to a name *)
 let paths = ref []
 
 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
+  paths := (p,name) :: !paths
 
 (* turn A/B/C into A.B.C *)
-let name_of_path = Str.global_replace (Str.regexp "/") ".";;
+let rec name_of_path p name fname suffix =
+  let dir = Filename.dirname fname in
+  if dir = fname then raise Not_found
+  else
+    let base = Filename.basename fname in
+    if p = dir then String.concat "." (name::base::suffix)
+    else name_of_path p name dir (base::suffix)
 
 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
+  let dirname, fname = normalize_filename bfname in
+  let rec change_prefix = function
+    (* Follow coqc: if in scope of -R, substitute logical name *)
+    (* otherwise, keep only base name *)
+    | [] -> fname
+    | (p, name) :: rem ->
+	try name_of_path p name dirname [fname]
+	with Not_found -> change_prefix rem
   in
-    change_prefix !paths nfname
+  change_prefix !paths
 
 let what_file f =
   check_if_file_exists f;
@@ -200,7 +194,7 @@ let files_from_file f =
       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;
+      eprintf "coqdoc: cannot read from file %s (%s)\n" f s;
       exit 1
     end
 
@@ -296,7 +290,7 @@ let parse () =
     | ("-toc-depth" | "--toc-depth") :: ds :: rem ->
       let d = try int_of_string ds with
                 Failure _ ->
-                  (eprintf "--toc-depth must be followed by an integer";
+                  (eprintf "--toc-depth must be followed by an integer\n";
                    exit 1)
       in
       Cdglobals.toc_depth := Some d;
@@ -404,13 +398,17 @@ let cat file =
       close_in c
 
 let copy src dst =
-  let cin = open_in src
-  and cout = open_out dst in
+  let cin = open_in src in
+  try
+    let 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
-
+      close_out cout;
+      close_in cin
+  with Sys_error e ->
+    eprintf "%s\n" e;
+    exit 1
 
 (*s Functions for generating output files *)
 
@@ -462,37 +460,35 @@ let gen_mult_files l =
     end
       (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
 
-let read_glob 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 e ->
-              eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e);
-	      x)
-  | Latex_file _ -> x
+let read_glob_file x =
+  try Index.read_glob x
+  with Sys_error s ->
+    eprintf "Warning: %s (links will not be available)\n" s
+
+let read_glob_file_of = function
+  | Vernac_file (f,_) -> read_glob_file (Filename.chop_extension f ^ ".glob")
+  | Latex_file _ -> ()
 
 let index_module = function
   | Vernac_file (f,m) ->
       Index.add_module m
   | Latex_file _ -> ()
 
+let copy_style_file file =
+  let src =
+    List.fold_left
+      Filename.concat !Cdglobals.coqlib_path ["tools";"coqdoc";file] in
+  let dst = coqdoc_out file in
+  if Sys.file_exists src then copy src dst
+  else eprintf "Warning: file %s does not exist\n" src
+
 let produce_document 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
-      if (Sys.file_exists src) then (copy src dst) else eprintf "Warning: file %s does not exist\n" src);
-  (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
-	if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src);
+  if !target_language=HTML then copy_style_file "coqdoc.css";
+  if !target_language=LaTeX then copy_style_file "coqdoc.sty";
   (match !Cdglobals.glob_source with
     | NoGlob -> ()
-    | DotGlob -> ignore (List.map read_glob l)
-    | GlobFile f -> ignore (Index.read_glob f));
+    | DotGlob -> List.iter read_glob_file_of l
+    | GlobFile f -> read_glob_file f);
   List.iter index_module l;
   match !out_to with
     | StdOut ->
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 515d9519f8..168a28f20b 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -187,6 +187,8 @@ module Latex = struct
       printf "\\end{document}\n"
     end
 
+  let nbsp () = output_char '~'
+
   let char c = match c with
     | '\\' ->
 	printf "\\symbol{92}"
@@ -304,7 +306,7 @@ module Latex = struct
     else
       with_latex_printing (fun s -> ident s l) s
 
-  let symbol s = with_latex_printing raw_ident s
+  let symbol s l = with_latex_printing raw_ident s
 
   let proofbox () = printf "\\ensuremath{\\Box}"
 
@@ -450,6 +452,8 @@ module Html = struct
   let empty_line_of_code () =
     printf "\n<br/>\n"
 
+  let nbsp () = printf "&nbsp;"
+
   let char = function
     | '<' -> printf "&lt;"
     | '>' -> printf "&gt;"
@@ -526,19 +530,25 @@ module Html = struct
 	    else (printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
       end
 
-  let with_html_printing f tok =
+  let with_html_printing f tok loc =
     try
       (match Hashtbl.find token_pp tok with
-	 | _, Some s -> output_string s
-	 | _ -> f tok)
+	 | _, Some s ->
+	     (try reference s (Index.find (get_module false) loc)
+	      with Not_found -> output_string s)
+	 | _ -> f tok loc)
     with Not_found ->
-      f tok
+      f tok loc
 
   let ident s l =
-    with_html_printing (fun s -> ident s l) s
+    with_html_printing ident s l
 
-  let symbol s =
-    with_html_printing raw_ident s
+  let raw_symbol s loc =
+    try reference s (Index.find (get_module false) loc)
+    with Not_found -> raw_ident s
+
+  let symbol s l =
+    with_html_printing raw_symbol s l
 
   let proofbox () = printf "<font size=-2>&#9744;</font>"
 
@@ -614,10 +624,11 @@ module Html = struct
   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;
+      printf "<a name=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat;
       List.iter
-	(fun (id,(text,link)) ->
-	   printf "<a href=\"%s\">%s</a> %s<br/>\n" link id text) l;
+	(fun (id,(text,link,t)) ->
+	   let id' = prepare_entry id t in
+	   printf "<a href=\"%s\">%s</a> %s<br/>\n" link id' text) l;
       printf "<br/><br/>"
     end
 
@@ -628,24 +639,24 @@ module Html = struct
   let format_global_index =
     Index.map
       (fun s (m,t) ->
-	 if t = Library then
+	if t = Library then
          let ln = !lib_name in
            if ln <> "" then
-	       "[" ^ String.lowercase ln ^ "]", m ^ ".html"
+	       "[" ^ String.lowercase ln ^ "]", m ^ ".html", t
            else
-	       "[library]", m ^ ".html"
-	 else
-	   sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
-	 sprintf "%s.html#%s" m s)
+	       "[library]", m ^ ".html", t
+	else
+	 sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
+	sprintf "%s.html#%s" m s, t)
 
   let format_bytype_index = function
     | Library, idx ->
-	Index.map (fun id m -> "", m ^ ".html") idx
+	Index.map (fun id m -> "", m ^ ".html", Library) 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
+	       (text, sprintf "%s.html#%s" m s, t)) idx
 
   (* Impression de la table d'index *)
   let print_index_table_item i =
@@ -653,9 +664,10 @@ module Html = struct
     List.iter
       (fun (c,l) ->
 	 if l <> [] then
-	   printf "<td><a href=\"%s\">%c</a></td>\n" (index_ref i c) c
+	   printf "<td><a href=\"%s\">%s</a></td>\n" (index_ref i c)
+	     (display_letter c)
 	 else
-	   printf "<td>%c</td>\n" c)
+	   printf "<td>%s</td>\n" (display_letter c))
       i.idx_entries;
     let n = i.idx_size in
       printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry");
@@ -667,7 +679,7 @@ module Html = struct
     printf "</table>\n"
 
   let make_one_multi_index prt_tbl i =
-    (* Attn: make_one_multi_index créé un nouveau fichier... *)
+    (* Attn: make_one_multi_index crée un nouveau fichier... *)
     let idx = i.idx_name in
     let one_letter ((c,l) as cl) =
       open_out_file (sprintf "%s_%s_%c.html" !index_name idx c);
@@ -750,6 +762,8 @@ module TeXmacs = struct
 
   let trailer () = ()
 
+  let nbsp () = output_char ' '
+
   let char_true c = match c with
     | '\\' -> printf "\\\\"
     | '<' -> printf "\\<"
@@ -806,7 +820,7 @@ module TeXmacs = struct
 	| "|-" -> ensuremath "vdash"
 	| s    -> raw_ident s
 
-  let symbol s = if !in_doc then symbol_true s else raw_ident s
+  let symbol s _ = if !in_doc then symbol_true s else raw_ident s
 
   let proofbox () = printf "QED"
 
@@ -891,6 +905,8 @@ module Raw = struct
 
   let trailer () = ()
 
+  let nbsp () = output_char ' '
+
   let char = output_char
 
   let label_char c = match c with
@@ -923,7 +939,7 @@ module Raw = struct
 
   let ident s loc = raw_ident s
 
-  let symbol s = raw_ident s
+  let symbol s loc = raw_ident s
 
   let proofbox () = printf "[]"
 
@@ -1028,6 +1044,7 @@ let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item Raw.stop
 let reach_item_level = select Latex.reach_item_level Html.reach_item_level TeXmacs.reach_item_level Raw.reach_item_level
 let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
 
+let nbsp = select Latex.nbsp Html.nbsp TeXmacs.nbsp Raw.nbsp
 let char = select Latex.char Html.char TeXmacs.char Raw.char
 let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
 let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index f8a25285c5..1ccbac2f94 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -60,9 +60,10 @@ val reach_item_level : int -> unit
 
 val rule : unit -> unit
 
+val nbsp : unit -> unit
 val char : char -> unit
 val ident : string -> loc -> unit
-val symbol : string -> unit
+val symbol : string -> loc -> unit
 
 val proofbox : unit -> unit