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

32 files changed, 753 insertions, 752 deletions

diff --git a/.gitignore b/.gitignore
index e96978b4c..79cdd99f7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -90,7 +90,6 @@ plugins/dp/dp_zenon.ml
 tools/gallina_lexer.ml
 tools/coqwc.ml
 tools/coqdep_lexer.ml
-tools/coqdoc/index.ml
 tools/coqdoc/cpretty.ml
 
 # .mly files
diff --git a/CHANGES b/CHANGES
index 4168ac3a0..6feef7794 100644
--- a/CHANGES
+++ b/CHANGES
@@ -144,6 +144,7 @@ Coqdoc
 - New option "--interpolate" to try and typeset identifiers in Coq escapings
   using the available globalization information.
 - New option "--external url root" to refer to external libraries.
+- Links to section variables and notations now supported.
 
 Library
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 009a21965..eb1d1985f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -337,7 +337,7 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
 let intern_notation intern (_,_,tmp_scope,scopes as env) loc ntn fullargs =
   let ntn,(args,argslist as fullargs) = contract_notation ntn fullargs in
   let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in
-  Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) df;
+  Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
   let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl argslist in
   subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c
@@ -383,9 +383,8 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
   with Not_found ->
   (* Is [id] bound in current env or is an ltac var bound to constr *)
   if Idset.mem id env or List.mem id vars1
-  then (
-    Dumpglob.dump_reference loc "<>" (string_of_id id) "var";
-    RVar (loc,id), [], [], [])
+  then
+    RVar (loc,id), [], [], []
   (* Is [id] a notation variable *)
   else if List.mem_assoc id vars3
   then
@@ -404,7 +403,10 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
 	(* [id] a section variable *)
 	(* Redundant: could be done in intern_qualid *)
 	let ref = VarRef id in
-	  RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, []
+	let impls = implicits_of_global ref in
+	let scopes = find_arguments_scope ref in
+	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
+	RRef (loc, ref), impls, scopes, []
       with _ ->
 	(* [id] a goal variable *)
 	RVar (loc,id), [], [], []
@@ -811,7 +813,7 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
   | CPatNotation (loc, ntn, fullargs) ->
       let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
       let (((ids',idsl'),c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-      Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) df;
+      Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
       let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
       let ids'',pl =
@@ -820,9 +822,8 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
       in ids@ids'', pl
   | CPatPrim (loc, p) ->
       let a = alias_of aliases in
-      let (c,df) = Notation.interp_prim_token_cases_pattern loc p a
+      let (c,_) = Notation.interp_prim_token_cases_pattern loc p a
 	(tmp_scope,scopes) in
-      Dumpglob.dump_notation_location (fst (unloc loc)) df;
       (ids,[asubst,c])
   | CPatDelimiters (loc, key, e) ->
       intern_pat (find_delimiters_scope loc key::scopes) aliases None e
@@ -1118,9 +1119,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CGeneralization (loc,b,a,c) ->
         intern_generalization intern env lvar loc b a c
     | CPrim (loc, p) ->
-	let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
-	Dumpglob.dump_notation_location (fst (unloc loc)) df;
-	c
+	fst (Notation.interp_prim_token loc p (tmp_scope,scopes))
     | CDelimiters (loc, key, e) ->
 	intern (ids,unb,None,find_delimiters_scope loc key::scopes) e
     | CAppExpl (loc, (isproj,ref), args) ->
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 9faea5406..519f902ba 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -47,23 +47,10 @@ let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output; glob_output := NoGlob
 let continue () = glob_output := !previous_state
 
+type coqdoc_state = Lexer.location_table
 
-let token_number = ref 0
-let last_pos = ref 0
-
-type coqdoc_state = Lexer.location_table * int * int
-
-let coqdoc_freeze () =
-  let lt = Lexer.location_table() in
-  let state = (lt,!token_number,!last_pos) in
-    token_number := 0;
-    last_pos := 0;
-    state
-
-let coqdoc_unfreeze (lt,tn,lp) =
-  Lexer.restore_location_table lt;
-  token_number := tn;
-  last_pos := lp
+let coqdoc_freeze = Lexer.location_table
+let coqdoc_unfreeze = Lexer.restore_location_table
 
 open Decl_kinds
 
@@ -200,19 +187,31 @@ let dump_libref loc dp ty =
   dump_string (Printf.sprintf "R%d %s <> <> %s\n"
 		  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
 
-let dump_notation_location pos ((path,df),sc) =
+let cook_notation df sc =
+  let ntn = String.make (String.length df * 3) '_' in
+  let j = ref 0 in
+  let quoted = ref false in
+  for i = 0 to String.length df - 1 do
+    if df.[i] = '\'' then quoted := not !quoted;
+    if df.[i] = ' ' then (ntn.[!j] <- '_'; incr j) else
+    if df.[i] = '_' && not !quoted then (ntn.[!j] <- 'x'; incr j) else
+    if df.[i] = 'x' && not !quoted then (String.blit "'x'" 0 ntn !j 3; j := !j + 3) else
+    (ntn.[!j] <- df.[i]; incr j)
+  done;
+  let df = String.sub ntn 0 !j in
+  match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
+
+let dump_notation (loc,(df,_)) sc sec =
+  (* We dump the location of the opening '"' *)
+  dump_string (Printf.sprintf "not %d %s %s\n" (fst (Util.unloc loc))
+    (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc))
+
+let dump_notation_location posl df (((path,secpath),_),sc) =
   if dump () then
-    let rec next growing =
-      let loc = Lexer.location_function !token_number in
-      let (bp,_) = Util.unloc loc in
-	if growing then if bp >= pos then loc else (incr token_number; next true)
-	else if bp = pos then loc
-	else if bp > pos then (decr token_number;next false)
-	else (incr token_number;next true) in
-    let loc = next (pos >= !last_pos) in
-      last_pos := pos;
-      let path = Names.string_of_dirpath path in
-      let _sc = match sc with Some sc -> " "^sc | _ -> "" in
-	dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
-
-
+    let path = Names.string_of_dirpath path in
+    let secpath = Names.string_of_dirpath secpath in
+    let df = cook_notation df sc in
+    List.iter (fun (bl,el) ->
+      for pos=bl to el do
+	dump_string (Printf.sprintf "R%d %s %s %s not\n" pos path secpath df)
+      done) posl
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 2f36c25c5..f6d7baefe 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -23,8 +23,9 @@ val dump_to_dotglob : unit -> unit
 val pause : unit -> unit
 val continue : unit -> unit
 
-val coqdoc_freeze : unit -> Lexer.location_table * int * int
-val coqdoc_unfreeze : Lexer.location_table * int * int -> unit
+type coqdoc_state = Lexer.location_table
+val coqdoc_freeze : unit -> coqdoc_state
+val coqdoc_unfreeze : coqdoc_state -> unit
 
 val add_glob : Util.loc -> Libnames.global_reference -> unit
 val add_glob_kn : Util.loc -> Names.kernel_name -> unit
@@ -34,8 +35,9 @@ val dump_moddef : Util.loc -> Names.module_path -> string -> unit
 val dump_modref  : Util.loc -> Names.module_path -> string -> unit
 val dump_reference  : Util.loc -> string -> string -> string -> unit
 val dump_libref : Util.loc -> Names.dir_path -> string -> unit
-val dump_notation_location : int -> (Notation.notation_location * Topconstr.scope_name option) -> unit
+val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation.notation_location * Topconstr.scope_name option) -> unit
 val dump_binding : Util.loc -> Names.Idset.elt -> unit
+val dump_notation : Util.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit
 val dump_constraint :  Topconstr.typeclass_constraint -> bool -> string -> unit
 val dump_local_binder : Topconstr.local_binder -> bool -> string -> unit
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 39ae27823..bee6c5c93 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -42,7 +42,7 @@ open Ppextend
 
 type level = precedence * tolerability list
 type delimiters = string
-type notation_location = dir_path * string
+type notation_location = (dir_path * dir_path) * string
 
 type scope = {
   notations: (string, interpretation * notation_location) Gmap.t;
@@ -355,7 +355,7 @@ let find_prim_token g loc p sc =
   (* Try for a primitive numerical notation *)
   let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
   check_required_module loc sc spdir;
-  g (interp ()), (dirpath (fst spdir),"")
+  g (interp ()), ((dirpath (fst spdir),empty_dirpath),"")
 
 let interp_prim_token_gen g loc p local_scopes =
   let scopes = make_current_scopes local_scopes in
@@ -536,6 +536,7 @@ type symbol =
 
 let rec string_of_symbol = function
   | NonTerminal _ -> ["_"]
+  | Terminal "_" -> ["'_'"]
   | Terminal s -> [s]
   | SProdList (_,l) ->
      let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"]
diff --git a/interp/notation.mli b/interp/notation.mli
index 3dc3c95c2..d549bb387 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -65,7 +65,7 @@ val find_delimiters_scope : loc -> delimiters -> scope_name
    negative numbers are not supported, the interpreter must fail with
    an appropriate error message *)
 
-type notation_location = dir_path * string
+type notation_location = (dir_path * dir_path) * string
 type required_module = full_path * string list
 type cases_pattern_status = bool (* true = use prim token in patterns *)
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a20cd1bc2..c0b624110 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1015,9 +1015,17 @@ type 'a module_signature =
   | Enforce of 'a (* ... : T *)
   | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
 
-let loc_of_notation f loc (args,_) ntn =
-  if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
-  else snd (Util.unloc (f (List.hd args)))
-
-let ntn_loc = loc_of_notation constr_loc
-let patntn_loc = loc_of_notation cases_pattern_expr_loc
+(* Returns the ranges of locs of the notation that are not occupied by args  *)
+(* and which are them occupied by proper symbols of the notation (or spaces) *)
+
+let locs_of_notation f loc (args,argslist) ntn =
+  let (bl,el) = Util.unloc loc in
+  let rec aux pos = function
+    | [] -> if pos = el then [] else [(pos,el-1)]
+    | a::l ->
+	let ba,ea = Util.unloc (f a) in
+	if pos = ba then aux ea l else (pos,ba-1)::aux ea l
+  in aux bl (args@List.flatten argslist)
+
+let ntn_loc = locs_of_notation constr_loc
+let patntn_loc = locs_of_notation cases_pattern_expr_loc
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 3b5832f18..2f25be94c 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -252,5 +252,8 @@ type 'a module_signature =
   | Enforce of 'a (* ... : T *)
   | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
 
-val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int
-val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int
+val ntn_loc :
+  Util.loc -> constr_expr notation_substitution -> string -> (int * int) list
+val patntn_loc :
+  Util.loc -> cases_pattern_expr notation_substitution -> string ->
+  (int * int) list
diff --git a/library/decls.ml b/library/decls.ml
index 251c86aba..ac2203ccf 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -36,6 +36,10 @@ let variable_opacity id = let (_,opaq,_,_) = Idmap.find id !vartab in opaq
 let variable_kind id = let (_,_,_,k) = Idmap.find id !vartab in k
 let variable_constraints id = let (_,_,cst,_) = Idmap.find id !vartab in cst
 
+let variable_secpath id =
+  let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
+  make_qualid dir id
+
 let variable_exists id = Idmap.mem id !vartab
 
 (** Datas associated to global parameters and constants *)
diff --git a/library/decls.mli b/library/decls.mli
index a9000604f..29fa13ae5 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -10,15 +10,7 @@
 
 open Names
 open Sign
-(*
 open Libnames
-open Term
-open Declarations
-open Entries
-open Indtypes
-open Safe_typing
-open Nametab
-*)
 open Decl_kinds
 
 (** This module manages non-kernel informations about declarations. It
@@ -31,6 +23,8 @@ type variable_data =
     dir_path * bool (* opacity *) * Univ.constraints * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
+val variable_path : variable -> dir_path
+val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
 val variable_constraints : variable -> Univ.constraints
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 8446bf50c..6e7acd3f5 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -36,7 +36,7 @@ let my_int_of_string loc s =
 GEXTEND Gram
   GLOBAL:
     bigint natural integer identref name ident var preident
-    fullyqualid qualid reference dirpath
+    fullyqualid qualid reference dirpath ne_lstring
     ne_string string pattern_ident pattern_identref by_notation smart_global;
   preident:
     [ [ s = IDENT -> s ] ]
@@ -99,6 +99,9 @@ GEXTEND Gram
         if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s
     ] ]
   ;
+  ne_lstring:
+    [ [ s = ne_string -> (loc,s) ] ]
+  ;
   dirpath:
     [ [ id = ident; l = LIST0 field ->
         make_dirpath (l@[id]) ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a153762ce..a0f9dcaef 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -238,7 +238,7 @@ GEXTEND Gram
       | -> None ] ]
   ;
   one_decl_notation:
-    [ [ ntn = ne_string; ":="; c = constr;
+    [ [ ntn = ne_lstring; ":="; c = constr;
         scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ]
   ;
   decl_notation:
@@ -844,7 +844,7 @@ GEXTEND Gram
 	 VernacArgumentsScope (use_section_locality (),qid,scl)
 
      | IDENT "Infix"; local = obsolete_locality;
-	 op = ne_string; ":="; p = constr;
+	 op = ne_lstring; ":="; p = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
          VernacInfix (enforce_module_locality local,(op,modl),p,sc)
@@ -853,7 +853,7 @@ GEXTEND Gram
 	 b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
            VernacSyntacticDefinition
 	     (id,(idl,c),enforce_module_locality local,b)
-     | IDENT "Notation"; local = obsolete_locality; s = ne_string; ":=";
+     | IDENT "Notation"; local = obsolete_locality; s = ne_lstring; ":=";
 	 c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
@@ -863,13 +863,14 @@ GEXTEND Gram
 	 pil = LIST1 production_item; ":="; t = Tactic.tactic
          -> VernacTacticNotation (n,pil,t)
 
-     | IDENT "Reserved"; IDENT "Infix"; s = ne_string;
+     | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
 	   Metasyntax.check_infix_modifiers l;
-	   VernacSyntaxExtension (use_module_locality (),("x '"^s^"' y",l))
+	   let (loc,s) = s in
+	   VernacSyntaxExtension (use_module_locality(),((loc,"x '"^s^"' y"),l))
 
      | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
-	 s = ne_string;
+	 s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
 	 -> VernacSyntaxExtension (enforce_module_locality local,(s,l))
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 1b53772f4..7120f72d2 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -292,6 +292,7 @@ module Prim =
     let dirpath = Gram.Entry.create "Prim.dirpath"
 
     let ne_string = Gram.Entry.create "Prim.ne_string"
+    let ne_lstring = Gram.Entry.create "Prim.ne_lstring"
 
   end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 6d5455b1b..ed370a995 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -186,6 +186,7 @@ module Prim :
     val smart_global : reference or_by_notation Gram.Entry.e
     val dirpath : dir_path Gram.Entry.e
     val ne_string : string Gram.Entry.e
+    val ne_lstring : string located Gram.Entry.e
     val var : identifier located Gram.Entry.e
   end
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 76b52dc33..ff480a5d4 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -285,7 +285,7 @@ let pr_type_option pr_c = function
   | CHole (loc, k) -> mt()
   | _ as c -> brk(0,2) ++ str":" ++ pr_c c
 
-let pr_decl_notation prc (ntn,c,scopt) =
+let pr_decl_notation prc ((loc,ntn),c,scopt) =
   fnl () ++ str "where " ++ qs ntn ++ str " := " ++ prc c ++
   pr_opt (fun sc -> str ": " ++ str sc) scopt
 
@@ -552,14 +552,14 @@ let rec pr_vernac = function
     pr_section_locality local ++ str"Arguments Scope" ++ spc() ++ 
     pr_smart_global q
     ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
-  | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *)
+  | VernacInfix (local,((_,s),mv),q,sn) -> (* A Verifier *)
       hov 0 (hov 0 (pr_locality local ++ str"Infix "
       ++ qs s ++ str " :=" ++ pr_constrarg q) ++
       pr_syntax_modifiers mv ++
       (match sn with
     | None -> mt()
     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
-  | VernacNotation (local,c,(s,l),opt) ->
+  | VernacNotation (local,c,((_,s),l),opt) ->
       let ps =
 	let n = String.length s in
 	if n > 2 & s.[0] = '\'' & s.[n-1] = '\''
@@ -573,7 +573,7 @@ let rec pr_vernac = function
         | None -> mt()
         | Some sc -> str" :" ++ spc() ++ str sc))
   | VernacSyntaxExtension (local,(s,l)) ->
-      pr_locality local ++ str"Reserved Notation" ++ spc() ++ qs s ++
+      pr_locality local ++ str"Reserved Notation" ++ spc() ++ pr_located qs s ++
       pr_syntax_modifiers l
 
   (* Gallina *)
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 24c5a1266..1424618f0 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -49,7 +49,7 @@ type fixpoint_kind =
   | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
   | IsCoFixpoint
 
-type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
+type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list
 
 type program_info = {
   prg_name: identifier;
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index aed5b58b7..bc5fc3e10 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -30,7 +30,7 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types ->
   ?reduce:(Term.constr -> Term.constr) ->
   ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress
 
-type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
+type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list
 
 type fixpoint_kind =
   | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
diff --git a/test-suite/coqdoc/links.v b/test-suite/coqdoc/links.v
new file mode 100644
index 000000000..b09d64a9a
--- /dev/null
+++ b/test-suite/coqdoc/links.v
@@ -0,0 +1,102 @@
+(** Various checks for coqdoc
+
+- symbols should not be inlined in string g
+- links to both kinds of notations in a' should work to the right notation
+- with utf8 option, forall must be unicode
+- spliting between symbols and ident should be correct in a' and c
+- ".." should be rendered correctly
+*)
+
+Require Import String.
+
+Definition g := "dfjkh""sdfhj forall <> * ~"%string.
+
+Definition a (b: nat) := b.
+
+Definition f := forall C:Prop, C.
+
+Notation "n ++ m" := (plus n m).
+
+Notation "n ++ m" := (mult n m). (* redefinition *)
+
+Notation "n % m" := (plus n m) (at level 60).
+
+Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).
+
+Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : x = x :>A
+
+where "x = y :> A" := (@eq A x y) : type_scope.
+
+Definition eq0 := 0 = 0 :> nat.
+
+Notation "( x # y ; .. ; z )" := (pair .. (pair x y) .. z).
+
+Definition p := ((0#0;0) , (0 % 0)).
+
+Notation h := a.
+
+  Section test.
+
+    Variables b' b2: nat.
+
+    Notation "n + m" := (plus n m) : my_scope.
+
+    Delimit Scope my_scope with my.
+
+    Notation l := 0.
+
+    Definition α := (0 + l)%my.
+
+    Definition a' b := b'++0++b2 _ ++x b.
+
+    Definition c := {True}+{True}.
+
+    Definition d := (1+2)%nat.
+
+    Lemma e : nat + nat.
+    Admitted.
+
+  End test.
+
+  Section test2.
+
+    Variables b': nat.
+
+    Section test.
+
+      Variables b2: nat.
+
+      Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.
+
+    End test.
+
+  End test2.
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index fe26e0086..d25034f2a 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 4994a1280..b2e23657b 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 071b3d555..97d581048 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 000000000..434a8bf5b
--- /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 3649d6a4a..517ec97a7 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 fe3b946e5..000000000
--- 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 7fb9322d7..fb9b64b4f 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 515d9519f..168a28f20 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 f8a25285c..1ccbac2f9 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
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a75ee2a7d..06b751c5f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -867,7 +867,7 @@ let compute_syntax_data (df,modifiers) =
   let typs = List.map (set_entry_type etyps) typs in
   let prec = (n,List.map (assoc_of_type n) typs) in
   let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in
-  let df' = (Lib.library_dp(),df) in
+  let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
   let i_data = (onlyparse,extrarecvars,recvars,vars,(ntn_for_interp,df')) in
   (i_data,sy_data)
 
@@ -974,7 +974,8 @@ let add_notation_in_scope local df c mods scope =
   let (acvars,ac) = interp_aconstr (vars,recvars) c in
   let a = (remove_extravars extrarecvars acvars,ac) in
   let onlyparse = onlyparse or is_not_printable ac in
-  Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'))
+  Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'));
+  df'
 
 let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse =
   let dfs = split_notation_string df in
@@ -985,55 +986,62 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
     Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules))
   end;
   (* Declare interpretation *)
-  let df' = (make_notation_key symbs,(Lib.library_dp(),df)) in
+  let path = (Lib.library_dp(),Lib.current_dirpath true) in
+  let df' = (make_notation_key symbs,(path,df)) in
   let (acvars,ac) = interp_aconstr ~impls (vars,recvars) c in
   let a = (remove_extravars extrarecvars acvars,ac) in
   let onlyparse = onlyparse or is_not_printable ac in
-  Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'))
+  Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'));
+  df'
 
 (* Notations without interpretation (Reserved Notation) *)
 
-let add_syntax_extension local mv =
-  let (_,sy_data) = compute_syntax_data mv in
+let add_syntax_extension local ((loc,df),mods) =
+  let (_,sy_data) = compute_syntax_data (df,mods) in
   let sy_rules = make_syntax_rules sy_data in
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
 
 (* Notations with only interpretation *)
 
-let add_notation_interpretation (df,c,sc) =
-  add_notation_interpretation_core false df c sc false
+let add_notation_interpretation ((loc,df),c,sc) =
+  let df' = add_notation_interpretation_core false df c sc false in
+  Dumpglob.dump_notation (loc,df') sc true
 
-let set_notation_for_interpretation impls (df,c,sc) =
-  (try silently (add_notation_interpretation_core false df ~impls c sc) false;
+let set_notation_for_interpretation impls ((_,df),c,sc) =
+  (try ignore
+    (silently (add_notation_interpretation_core false df ~impls c sc) false);
   with NoSyntaxRule ->
     error "Parsing rule for this notation has to be previously declared.");
   Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
 
 (* Main entry point *)
 
-let add_notation local c (df,modifiers) sc =
-  if no_syntax_modifiers modifiers then
+let add_notation local c ((loc,df),modifiers) sc =
+  let df' =
+   if no_syntax_modifiers modifiers then
     (* No syntax data: try to rely on a previously declared rule *)
     let onlyparse = modifiers=[SetOnlyParsing] in
     try add_notation_interpretation_core local df c sc onlyparse
     with NoSyntaxRule ->
       (* Try to determine a default syntax rule *)
       add_notation_in_scope local df c modifiers sc
-  else
+   else
     (* Declare both syntax and interpretation *)
     add_notation_in_scope local df c modifiers sc
+  in
+  Dumpglob.dump_notation (loc,df') sc true
 
 (* Infix notations *)
 
 let inject_var x = CRef (Ident (dummy_loc, id_of_string x))
 
-let add_infix local (inf,modifiers) pr sc =
+let add_infix local ((loc,inf),modifiers) pr sc =
   check_infix_modifiers modifiers;
   (* check the precedence *)
   let metas = [inject_var "x"; inject_var "y"] in
   let c = mkAppC (pr,metas) in
   let df = "x "^(quote_notation_token inf)^" y" in
-  add_notation local c (df,modifiers) sc
+  add_notation local c ((loc,df),modifiers) sc
 
 (**********************************************************************)
 (* Delimiters and classes bound to scopes                             *)
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 01c0a34da..a06806935 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -29,11 +29,11 @@ val add_tactic_notation :
 
 (* Adding a (constr) notation in the environment*)
 
-val add_infix : locality_flag -> (string * syntax_modifier list) ->
+val add_infix : locality_flag -> (lstring * syntax_modifier list) ->
   constr_expr -> scope_name option -> unit
 
 val add_notation : locality_flag -> constr_expr ->
-  (string * syntax_modifier list) -> scope_name option -> unit
+  (lstring * syntax_modifier list) -> scope_name option -> unit
 
 (* Declaring delimiter keys and default scopes *)
 
@@ -43,17 +43,17 @@ val add_class_scope : scope_name -> Classops.cl_typ -> unit
 (* Add only the interpretation of a notation that already has pa/pp rules *)
 
 val add_notation_interpretation :
-  (string * constr_expr * scope_name option) -> unit
+  (lstring * constr_expr * scope_name option) -> unit
 
 (* Add a notation interpretation for supporting the "where" clause *)
 
 val set_notation_for_interpretation : Constrintern.full_internalization_env ->
-  (string * constr_expr * scope_name option) -> unit
+  (lstring * constr_expr * scope_name option) -> unit
 
 (* Add only the parsing/printing rule of a notation *)
 
 val add_syntax_extension :
-  locality_flag -> (string * syntax_modifier list) -> unit
+  locality_flag -> (lstring * syntax_modifier list) -> unit
 
 (* Add a syntactic definition (as in "Notation f := ...") *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f299f3a51..c077fc492 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -756,7 +756,8 @@ let vernac_declare_tactic_definition (local,x,def) =
 let vernac_create_hintdb local id b =
   Auto.create_hint_db local id full_transparent_state b
 
-let vernac_hints local lb h = Auto.add_hints local lb (Auto.interp_hints h)
+let vernac_hints local lb h =
+  Auto.add_hints local lb (Auto.interp_hints h)
 
 let vernac_syntactic_definition lid =
   Dumpglob.dump_definition lid false "syndef";
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 3c9774a16..4f7beeb0b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -26,7 +26,7 @@ open Nametab
 
 type lident = identifier located
 type lname = name located
-type lstring = string
+type lstring = string located
 type lreference = reference
 
 type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
@@ -160,7 +160,7 @@ type local_decl_expr =
   | DefExpr of lname * constr_expr * constr_expr option
 
 type inductive_kind = Inductive_kw | CoInductive | Record | Structure | Class of bool (* true = definitional, false = inductive *)
-type decl_notation = string * constr_expr * scope_name option
+type decl_notation = lstring * constr_expr * scope_name option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
 type 'a with_coercion = coercion_flag * 'a
@@ -202,7 +202,7 @@ type scheme =
 type vernac_expr =
   (* Control *)
   | VernacList of located_vernac_expr list
-  | VernacLoad of verbose_flag * lstring
+  | VernacLoad of verbose_flag * string
   | VernacTime of vernac_expr
   | VernacTimeout of int * vernac_expr
 
@@ -210,7 +210,7 @@ type vernac_expr =
   | VernacTacticNotation of int * grammar_tactic_prod_item_expr list * raw_tactic_expr
   | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
-  | VernacDelimiters of scope_name * lstring
+  | VernacDelimiters of scope_name * string
   | VernacBindScope of scope_name * class_rawexpr list
   | VernacArgumentsScope of locality_flag * reference or_by_notation *
       scope_name option list
@@ -285,16 +285,16 @@ type vernac_expr =
 
 
   (* Auxiliary file and library management *)
-  | VernacRequireFrom of export_flag option * specif_flag option * lstring
-  | VernacAddLoadPath of rec_flag * lstring * dir_path option
-  | VernacRemoveLoadPath of lstring
-  | VernacAddMLPath of rec_flag * lstring
-  | VernacDeclareMLModule of locality_flag * lstring list
-  | VernacChdir of lstring option
+  | VernacRequireFrom of export_flag option * specif_flag option * string
+  | VernacAddLoadPath of rec_flag * string * dir_path option
+  | VernacRemoveLoadPath of string
+  | VernacAddMLPath of rec_flag * string
+  | VernacDeclareMLModule of locality_flag * string list
+  | VernacChdir of string option
 
   (* State management *)
-  | VernacWriteState of lstring
-  | VernacRestoreState of lstring
+  | VernacWriteState of string
+  | VernacRestoreState of string
 
   (* Resetting *)
   | VernacRemoveName of lident
@@ -306,8 +306,8 @@ type vernac_expr =
   (* Commands *)
   | VernacDeclareTacticDefinition of
       (locality_flag * rec_flag * (reference * bool * raw_tactic_expr) list)
-  | VernacCreateHintDb of locality_flag * lstring * bool
-  | VernacHints of locality_flag * lstring list * hints_expr
+  | VernacCreateHintDb of locality_flag * string * bool
+  | VernacHints of locality_flag * string list * hints_expr
   | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * reference or_by_notation *