Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

10 files changed, 384 insertions, 249 deletions

diff --git a/tools/check-translate b/tools/check-translate
new file mode 100755
index 00000000..3dd82405
--- /dev/null
+++ b/tools/check-translate
@@ -0,0 +1,23 @@
+#!/bin/sh
+
+echo -------------- Producing translated files ---------------------
+rm */*/*.v8 >& /dev/null
+make COQ_XML=-translate theories || { echo ---- Failed to translate; exit 1; }
+if [ -e translated ]; then rm -r translated; fi
+if [ -e successful-translation ]; then rm -r successful-translation; fi
+if [ -e failed-translation ]; then rm -r failed-translation; fi
+mv theories translated
+mkdir theories
+echo -------------------- Upgrading files --------------------------
+cd translated
+for i in */*.v
+do
+  mkdir ../theories/`dirname $i` >& /dev/null
+  mv "$i"8 ../theories/$i
+done
+cd ..
+echo --------------- Recompiling translated files ------------------
+make theories || { echo ---- Failed to recompile; mv theories failed-translation; mv translated theories; exit 1; }
+echo ----------------- Recompilation successful --------------------
+if [ -e successful-translation ]; then rm -r successful-translation; fi
+mv theories successful-translation; mv translated theories
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index cc3e9515..cd9d3669 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_makefile.ml4 7994 2006-02-06 08:48:37Z herbelin $ *)
+(* $Id: coq_makefile.ml4 8840 2006-05-22 13:51:14Z notin $ *)
 
 (* créer un Makefile pour un développement Coq automatiquement *)
 
@@ -197,7 +197,7 @@ let variables l =
   print "COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
   print "COQC=$(COQBIN)coqc\n";
   print "GALLINA=gallina\n";
-  print "COQDOC=coqdoc\n";
+  print "COQDOC=$(COQBIN)coqdoc\n";
   print "CAMLC=ocamlc -c\n";
   print "CAMLOPTC=ocamlopt -c\n";
   print "CAMLLINK=ocamlc\n";
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index eb740712..6597c3f6 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml 8642 2006-03-17 10:09:02Z notin $ *)
+(* $Id: coqdep.ml 8923 2006-06-08 16:39:58Z herbelin $ *)
 
 open Printf
 open Coqdep_lexer
@@ -162,8 +162,12 @@ let sort () =
       try
 	while true do
 	  match coq_action lb with
-	    | Require (_, s) ->
-		(try loop (List.assoc s !vKnown) with Not_found -> ())
+	    | Require (_, sl) ->
+		List.iter 
+		  (fun s -> 
+		    try loop (List.assoc s !vKnown) 
+		    with Not_found -> ())
+		sl
 	    | RequireString (_, s) -> loop s
 	    | _ -> ()
 	done
@@ -184,17 +188,18 @@ let traite_fichier_Coq verbose f =
       while true do
       	let tok = coq_action buf in
 	match tok with
-	  | Require (spec,str) ->
-	      if not (List.mem str !deja_vu_v) then begin
-	        addQueue deja_vu_v str;
-                try
-                  let file_str = safe_assoc verbose f str in
-                  printf " %s%s" (canonize file_str)
-                    (if spec then !suffixe_spec else !suffixe)
-                with Not_found -> 
-		  if verbose && not (List.mem_assoc str !coqlibKnown) then
-                    warning_module_notfound f str
-       	      end
+	  | Require (spec,strl) ->
+	      List.iter (fun str ->
+		if not (List.mem str !deja_vu_v) then begin
+	          addQueue deja_vu_v str;
+                  try
+                    let file_str = safe_assoc verbose f str in
+                    printf " %s%s" (canonize file_str)
+                      (if spec then !suffixe_spec else !suffixe)
+                  with Not_found -> 
+		    if verbose && not (List.mem_assoc str !coqlibKnown) then
+                      warning_module_notfound f str
+       		end) strl
 	  | RequireString (spec,s) -> 
 	      let str = Filename.basename s in
 	      if not (List.mem [str] !deja_vu_v) then begin
@@ -332,7 +337,7 @@ let mL_dependencies () =
        flush stdout)
     (List.rev !mlAccu);
   List.iter
-    (fun ((name,ext,dirname) as pairname) ->
+    (fun ((name,ext,dirname)) ->
        let fullname = file_name ([name],dirname) in
        let (dep,_) = traite_fichier_ML fullname ext in
        printf "%s.cmi: %s%s" fullname fullname ext;
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index f7f37086..8ecab3b4 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqdep_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: coqdep_lexer.mll 8737 2006-04-26 21:55:21Z herbelin $ i*)
   
 {
 
@@ -18,7 +18,7 @@
   type spec = bool
 		
   type coq_token = 
-    | Require of spec * string list
+    | Require of spec * string list list
     | RequireString of spec * string
     | Declare of string list
     | Load of string
@@ -27,7 +27,8 @@
  
   exception Fin_fichier
     
-  let module_name = ref []
+  let module_current_name = ref []
+  let module_names = ref []
   let ml_module_name = ref ""
 		      
   let specif = ref false
@@ -48,13 +49,11 @@ let dot = '.' ( space+ | eof)
 
 rule coq_action = parse
   | "Require" space+
-      { specif := false; opened_file lexbuf }
+      { specif := false; module_names := []; opened_file lexbuf }
   | "Require" space+ "Export" space+
-      { specif := false; opened_file lexbuf}
-  | "Require" space+ "Syntax" space+
-      { specif := false; opened_file lexbuf}
+      { specif := false; module_names := []; opened_file lexbuf}
   | "Require" space+ "Import" space+
-      { specif := false; opened_file lexbuf}
+      { specif := false; module_names := []; opened_file lexbuf}
   | "Declare" space+ "ML" space+ "Module" space+
       { mllist := []; modules lexbuf}
   | "Load" space+
@@ -175,7 +174,7 @@ and opened_file = parse
   | "Specification"
                 { specif := true; opened_file lexbuf }
   | coq_ident
-       	       	{ module_name := [Lexing.lexeme lexbuf];
+       	       	{ module_current_name := [Lexing.lexeme lexbuf];
                   opened_file_fields lexbuf }
 
   | '"' [^'"']* '"'   { (*'"'*)
@@ -186,23 +185,28 @@ and opened_file = parse
                             Filename.chop_suffix str ".v"
                           else str in
 			RequireString (!specif, str) }
-  | eof		      { raise Fin_fichier }
-  | _		      { opened_file lexbuf }
+  | eof         { raise Fin_fichier }
+  | _           { opened_file lexbuf }
 
 and opened_file_fields = parse
   | "(*" (* "*)" *)
                 { comment_depth := 1; comment lexbuf;
                   opened_file_fields lexbuf }
   | space+
-      	       	{ opened_file_fields lexbuf }
+                { opened_file_fields lexbuf }
   | coq_field
-       	       	{ module_name :=
-                    field_name (Lexing.lexeme lexbuf) :: !module_name;
+                { module_current_name :=
+                    field_name (Lexing.lexeme lexbuf) :: !module_current_name;
                   opened_file_fields lexbuf }
-  | dot               { Require (!specif, List.rev !module_name) }
-  | eof		      { raise Fin_fichier }
-  | _		      { opened_file_fields lexbuf }
-
+  | coq_ident   { module_names := 
+                    List.rev !module_current_name :: !module_names;
+                  module_current_name := [Lexing.lexeme lexbuf];
+                  opened_file_fields lexbuf }
+  | dot         { module_names :=
+                    List.rev !module_current_name :: !module_names;
+                  Require (!specif, List.rev !module_names) }
+  | eof         { raise Fin_fichier }
+  | _           { opened_file_fields lexbuf }
 
 and modules = parse
   | space+              { modules lexbuf }
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index b5a4cb22..8a774876 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -44,6 +44,7 @@ let page_title = ref ""
 let title = ref ""
 let externals = ref true
 let coqlib = ref "http://coq.inria.fr/library/"
+let coqlib_path = ref Coq_config.coqlib
 let raw_comments = ref false
 
 let charset = ref "iso-8859-1"
@@ -69,4 +70,3 @@ type file =
   | Vernac_file of string * coq_module
   | Latex_file of string
       
-
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index b59438e5..3900987e 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -28,16 +28,21 @@ body { padding: 0px 0px;
 
 #main  a.idref:visited {color : #416DFF; text-decoration : none; }
 #main  a.idref:link {color : #416DFF; text-decoration : none; }
-#main  a.idref:hover {color : Red; text-decoration : underline; }
-#main  a.idref:active {color : Red; text-decoration : underline; }
+#main  a.idref:hover {text-decoration : none; }
+#main  a.idref:active {text-decoration : none; }
 
-#main .keyword { font-weight : bold; 
-                 color : Red }
+#main  a.modref:visited {color : #416DFF; text-decoration : none; }
+#main  a.modref:link {color : #416DFF; text-decoration : none; }
+#main  a.modref:hover {text-decoration : none; }
+#main  a.modref:active {text-decoration : none; }
 
-#main .section { font-size : 20pt }
+#main .keyword { color : #cf1d1d }
+#main { color: black }
+
+#main .section { background-color:#899BD6;
+                 font-size : 20pt }
 
 #main code { font-family: monospace; 
-             font-size: 8pt; 
              line-height: 50% }
 
 #main .doc { margin: 0px;
@@ -45,10 +50,11 @@ body { padding: 0px 0px;
              font-family: sans-serif;
              font-size: 11pt;
              font-weight:bold;
-             background-color:#66ff66 }
+             color: black;
+             background-color: #90bdff;
+             border-style: plain}
 
-#main .doc code { font-family: monospace; 
-                  font-size: 10pt} 
+#main .doc code { font-family: monospace} 
 
 /* Pied de page */
 
@@ -56,4 +62,6 @@ body { padding: 0px 0px;
           font-family: sans-serif; }
 
 #footer a:visited { color: blue; }
+#footer a:link { text-decoration: none; 
+                 color: #888888; }
 
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index ec89da2f..9b5716ff 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mll 8617 2006-03-08 10:47:12Z notin $ i*)
+(*i $Id: index.mll 8863 2006-05-26 10:33:21Z notin $ i*)
 
 {
 
@@ -34,11 +34,14 @@ type index_entry =
   | Ref of coq_module * string
   | Mod of coq_module * string
 
-let table = Hashtbl.create 97
+let current_type = ref Library
+let current_library = ref ""
+  (** referes to the file being parsed *)
 
-let current_module = ref ""
+let table = Hashtbl.create 97
+  (** [table] is used to store references and definitions *)
 
-let add_def loc ty id = Hashtbl.add table (!current_module, loc) (Def (id, ty))
+let add_def loc ty id = Hashtbl.add table (!current_library, loc) (Def (id, ty))
 
 let add_ref m loc m' id = Hashtbl.add table (m, loc) (Ref (m', id))
 
@@ -46,7 +49,55 @@ let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
 
 let find m l = Hashtbl.find table (m, l)
 
-let current_type = ref Library
+
+(*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 *)
 
@@ -83,7 +134,7 @@ let ref_module loc s =
     let n = String.length s in
     let i = String.rindex s ' ' in 
     let id = String.sub s (i+1) (n-i-1) in
-    add_mod !current_module (loc+i+1) (Hashtbl.find modules id) id
+      add_mod !current_library (loc+i+1) (Hashtbl.find modules id) id
   with Not_found -> 
     ()
 
@@ -104,25 +155,25 @@ 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
-    
+    List.iter 
+      (fun c -> Hashtbl.add t c [])
+      ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N'; 
+       'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_'];  
+    List.iter 
+      (fun ((s,_) as e) -> 
+	 let c = Alpha.norm_char s.[0] in 
+	 let l = try Hashtbl.find t c with Not_found -> [] in
+	   Hashtbl.replace t c (e :: l)) 
+      el;
+    let res = ref [] in
+      Hashtbl.iter 
+	(fun c l -> res := (c, List.sort compare_entries l) :: !res) t;
+      List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res
+	
 let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
-
+  
 let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
-
+  
 let type_name = function
   | Library -> "library"
   | Module -> "module"
@@ -133,28 +184,28 @@ let type_name = function
   | Variable -> "variable"
   | Axiom -> "axiom"
   | TacticDefinition -> "tactic"
-
+      
 let all_entries () =
   let gl = ref [] in
   let add_g s m t = gl := (s,(m,t)) :: !gl in
   let bt = Hashtbl.create 11 in
   let add_bt t s m =
     let l = try Hashtbl.find bt t with Not_found -> [] in
-    Hashtbl.replace bt t ((s,m) :: l)
+      Hashtbl.replace bt t ((s,m) :: l)
   in
   let classify (m,_) e = match e with 
     | Def (s,t) -> add_g s m t; add_bt t s m
     | Ref _ | Mod _ -> ()
   in
-  Hashtbl.iter classify table;
-  Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
-  { idx_name = "global"; 
-    idx_entries = sort_entries !gl; 
-    idx_size = List.length !gl },
-  Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t; 
+    Hashtbl.iter classify table;
+    Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
+    { idx_name = "global"; 
+      idx_entries = sort_entries !gl; 
+      idx_size = List.length !gl },
+    Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t; 
 				   idx_entries = sort_entries e; 
 				   idx_size = List.length e }) :: l) bt []
-
+    
 }
 
 (*s Shortcuts for regular expressions. *)
@@ -165,15 +216,14 @@ let firstchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
 let identchar = 
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
-   '\'' '0'-'9']
-let ident = 
-  firstchar identchar*
+     '\'' '0'-'9']
+let ident = firstchar identchar*
 
 let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
 let end_hide = "(*" space* "end" space+ "hide" space* "*)"
-
+  
 (*s Indexing entry point. *)
-
+  
 rule traverse = parse
   | "Definition" space
       { current_type := Definition; index_ident lexbuf; traverse lexbuf }
@@ -192,13 +242,15 @@ rule traverse = parse
   | "Record" space
       { current_type := Inductive; index_ident lexbuf; traverse lexbuf }
   | "Module" (space+ "Type")? space
-      { current_type := Module; index_ident lexbuf; traverse lexbuf }
+      { 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"))? space+ ident
       { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf }
+  | "End" space+ 
+      { end_ident lexbuf; traverse lexbuf }
   | begin_hide 
       { skip_hide lexbuf; traverse lexbuf }
   | "(*" 
@@ -216,7 +268,16 @@ and index_ident = parse
   | space+ 
       { index_ident lexbuf }
   | ident  
-      { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf) }
+      { 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    
       { () }
   | _      
@@ -234,12 +295,12 @@ and index_idents = parse
       { () }
   | _
       { 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 }
+	{ current_type := Constructor; index_ident lexbuf; inductive lexbuf }
   | "with" space
       { current_type := Inductive; index_ident lexbuf; inductive lexbuf }
   | '.'    
@@ -248,9 +309,9 @@ and inductive = parse
       { () }
   | _      
       { inductive lexbuf }
-
+      
 (*s Index identifiers in a Fixpoint declaration. *)
-
+      
 and fixpoint = parse
   | "with" space
       { index_ident lexbuf; fixpoint lexbuf }
@@ -260,9 +321,9 @@ and fixpoint = parse
       { () }
   | _      
       { fixpoint lexbuf }
-
+      
 (*s Skip a possibly nested comment. *)
-
+      
 and comment = parse
   | "*)" { () }
   | "(*" { comment lexbuf; comment lexbuf }
@@ -271,25 +332,48 @@ and comment = parse
   | _    { 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 }
+  | ident space* ":="
+      { () }
+  | ident
+      { let id = lexeme lexbuf in
+	  begin_module id; add_def (lexeme_start lexbuf) !current_type id }
+  | eof
+      { () }
+  | _
+      { () }
+
 {
   
   let read_glob f = 
@@ -306,10 +390,11 @@ and skip_hide = parse
 	    | 'R' ->
 		(try
 		   let i = String.index s ' ' in
+		   let j = String.index_from s (i+1) ' ' in 
 		   let loc = int_of_string (String.sub s 1 (i - 1)) in
-		   let sp = String.sub s (i + 1) (n - i - 1) in
-		   let m',id = split_sp sp in
-		   add_ref !cur_mod loc m' id
+		   let lib_dp = String.sub s (i + 1) (j - i - 1) in
+		   let full_id = String.sub s (j + 1) (n - j - 1) in
+		     add_ref !cur_mod loc lib_dp full_id
 		 with Not_found -> 
 		   ())
 	    | _ -> ()
@@ -317,11 +402,11 @@ and skip_hide = parse
       done
     with End_of_file -> 
       close_in c
-
+	
   let scan_file f m = 
-    current_module := m;
+    init_stack (); current_library := m;
     let c = open_in f in
     let lb = from_channel c in
-    traverse lb;
-    close_in c
+      traverse lb;
+      close_in c
 }
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 177fc2bc..18a44a44 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 8669 2006-03-28 17:34:15Z notin $ i*)
+(*i $Id: main.ml 8777 2006-05-02 10:14:39Z notin $ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -54,6 +54,7 @@ let usage () =
   prerr_endline "  --no-externals      no links to Coq standard library";
   prerr_endline "  --coqlib <url>      set URL for Coq standard library";
   prerr_endline "                      (default is http://coq.inria.fr/library/)";
+  prerr_endline "  --coqlib_path <dir> set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>   map physical dir to Coq dir";
   prerr_endline "  --latin1            set ISO-8859-1 input language";
   prerr_endline "  --utf8              set UTF-8 input language";
@@ -71,12 +72,12 @@ let banner () =
   eprintf "This is coqdoc version %s, compiled on %s\n"
     Coq_config.version Coq_config.compile_date;
   flush stderr
-
+    
 let target_full_name f = 
   match !target_language with
     | HTML -> f ^ ".html"
     | _ -> f ^ ".tex"
-
+	
 (*s \textbf{Separation of files.} Files given on the command line are
     separated according to their type, which is determined by their
     suffix.  Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\
@@ -87,11 +88,11 @@ let check_if_file_exists f =
     eprintf "\ncoqdoc: %s: no such file\n" f;
     exit 1
   end
-
+    
 let paths = ref []
-
+  
 let add_path m l = paths := (m,l) :: !paths
-
+  
 let exists_dir dir =
   try let _ = Unix.opendir dir in true with Unix.Unix_error _ -> false
 
@@ -99,72 +100,72 @@ let add_rec_path f l =
   let rec traverse abs rel =
     add_path abs rel;
     let dirh = Unix.opendir abs in
-    try
-      while true do
-	let f = Unix.readdir dirh in
-	if f <> "" && f.[0] <> '.' && f <> "CVS" then
-	  let abs' = Filename.concat abs f in
-	  try 
-	    if exists_dir abs' then  traverse abs' (rel ^ "." ^ f)
-	  with Unix.Unix_error _ -> 
-	    ()
-      done
-    with End_of_file ->
-      Unix.closedir dirh
+      try
+	while true do
+	  let f = Unix.readdir dirh in
+	    if f <> "" && f.[0] <> '.' && f <> "CVS" then
+	      let abs' = Filename.concat abs f in
+		try 
+		  if exists_dir abs' then  traverse abs' (rel ^ "." ^ f)
+		with Unix.Unix_error _ -> 
+		  ()
+	done
+      with End_of_file ->
+	Unix.closedir dirh
   in
-  if exists_dir f then traverse f l
+    if exists_dir f then traverse f l
 
 (* turn A/B/C into A.B.C *)
 let make_path = Str.global_replace (Str.regexp "/") ".";;
 
 let coq_module file = 
-(* TODO
- * LEM:
- * We should also remove things like "/./" in the middle of the filename,
- * rewrite "/foo/../bar" to "/bar", recognise different paths that lead
- * to the same file / directory (via symlinks), etc. The best way to do
- * all this would be to use the libc function realpath() on _both_ p and
- * file / f before comparing them.
- *
- * The semantics of realpath() on file symlinks might not be what we
- * want... (But it is what we want on directory symlinks.) So, we would
- * have to cook up our own version of realpath()?
- *
- * Do all target platforms have realpath()?
- *)
+  (* TODO
+   * LEM:
+   * We should also remove things like "/./" in the middle of the filename,
+   * rewrite "/foo/../bar" to "/bar", recognise different paths that lead
+   * to the same file / directory (via symlinks), etc. The best way to do
+   * all this would be to use the libc function realpath() on _both_ p and
+   * file / f before comparing them.
+   *
+   * The semantics of realpath() on file symlinks might not be what we
+   * want... (But it is what we want on directory symlinks.) So, we would
+   * have to cook up our own version of realpath()?
+   *
+   * Do all target platforms have realpath()?
+   *)
   let f = chop_extension file in
-  (* remove leading ./ and any number of slashes after *)
+    (* remove leading ./ and any number of slashes after *)
   let f = Str.replace_first (Str.regexp "^\\./+") "" f in
-  if (Str.string_before f 1) = "/" then
-    (* f is an absolute path. Prefixes must be matched with the beginning of f,
-     * not prepended
-     *)
-    let rec trypath = function
-     | [] -> make_path f
-     | (p, lg) :: r ->
-         (* make sure p ends with a single '/'
-          * This guarantees that we don't match a file whose name is
-          * of the form p ^ "foo". It means we may miss p itself,
-          * but this does not matter: coqdoc doesn't do anything
-          * of a directory anyway. *)
-         let p = (Str.replace_first (Str.regexp "/*$") "/" p) in
-         let p_quoted = (Str.quote p) in
-         if (Str.string_match (Str.regexp p_quoted) f 0) then
-           make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f))
-        else
-           trypath r
-    in trypath !paths
-  else (* f is a relative path *)
-    let rec trypath = function
-      | [] -> 
-	  make_path f
-      | (p,lg) :: r ->
-	  let p_file = Filename.concat p file in
-	  if Sys.file_exists p_file then
-	    make_path (Filename.concat lg f)
-	  else
-	    trypath r
-    in trypath !paths;;
+    if (Str.string_before f 1) = "/" then
+      (* f is an absolute path. Prefixes must be matched with the beginning of f,
+       * not prepended
+       *)
+      let rec trypath = function
+	| [] -> make_path f
+	| (p, lg) :: r ->
+            (* make sure p ends with a single '/'
+             * This guarantees that we don't match a file whose name is
+             * of the form p ^ "foo". It means we may miss p itself,
+             * but this does not matter: coqdoc doesn't do anything
+             * of a directory anyway. *)
+            let p = (Str.replace_first (Str.regexp "/*$") "/" p) in
+            let p_quoted = (Str.quote p) in
+              if (Str.string_match (Str.regexp p_quoted) f 0) then
+		make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f))
+              else
+		trypath r
+      in trypath !paths
+    else (* f is a relative path *)
+      let rec trypath = function
+	| [] -> 
+	    make_path f
+	| (p,lg) :: r ->
+	    let p_file = Filename.concat p file in
+	      if Sys.file_exists p_file then
+		make_path (Filename.concat lg f)
+	      else
+		trypath r
+      in trypath !paths;;
 
 let what_file f =
   check_if_file_exists f;
@@ -176,43 +177,43 @@ let what_file f =
     eprintf "\ncoqdoc: don't know what to do with %s\n" f;
     exit 1
   end
-
+    
 (*s \textbf{Reading file names from a file.} 
-    File names may be given
-    in a file instead of being given on the command
-    line. [(files_from_file f)] returns the list of file names contained
-    in the file named [f]. These file names must be separated by spaces,
-    tabulations or newlines.
+ *  File names may be given
+ *  in a file instead of being given on the command
+ *  line. [(files_from_file f)] returns the list of file names contained
+ *  in the file named [f]. These file names must be separated by spaces,
+ *  tabulations or newlines.
  *)
 
 let files_from_file f =
   let files_from_channel ch =
     let buf = Buffer.create 80 in
     let l = ref [] in
-    try
-      while true do
-	match input_char ch with
-	  | ' ' | '\t' | '\n' ->
-	      if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
-	      Buffer.clear buf
-	  | c -> 
-	      Buffer.add_char buf c
-      done; []
-    with End_of_file ->
-      List.rev !l
+      try
+	while true do
+	  match input_char ch with
+	    | ' ' | '\t' | '\n' ->
+		if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
+		Buffer.clear buf
+	    | c -> 
+		Buffer.add_char buf c
+	done; []
+      with End_of_file ->
+	List.rev !l
   in
-  try
-    check_if_file_exists f;
-    let ch = open_in f in
-    let l = files_from_channel ch in
-    close_in ch;l
-  with Sys_error s -> begin
-    eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s;
-    exit 1
-  end
-
+    try
+      check_if_file_exists f;
+      let ch = open_in f in
+      let l = files_from_channel ch in
+	close_in ch;l
+    with Sys_error s -> begin
+      eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s;
+      exit 1
+    end
+      
 (*s \textbf{Parsing of the command line.} *)
-
+      
 let output_file = ref ""
 let dvi = ref false
 let ps = ref false
@@ -222,9 +223,9 @@ let parse () =
   let add_file f = files := f :: !files in
   let rec parse_rec = function
     | [] -> ()
-
+	
     | ("-nopreamble" | "--nopreamble" | "--no-preamble"
-    |  "-bodyonly"   | "--bodyonly"   | "--body-only") :: rem ->
+      |  "-bodyonly"   | "--bodyonly"   | "--body-only") :: rem ->
 	header_trailer := false; parse_rec rem
     | ("-p" | "--preamble") :: s :: rem ->
 	push_in_preamble s; parse_rec rem
@@ -239,7 +240,7 @@ let parse () =
     | ("-stdout" | "--stdout") :: rem ->
 	out_to := StdOut; parse_rec rem
     | ("-o" | "--output") :: f :: rem ->
-	out_to := File f; parse_rec rem
+	out_to := File (Filename.basename f); output_dir := Filename.dirname f; parse_rec rem
     | ("-o" | "--output") :: [] -> 
 	usage ()
     | ("-d" | "--directory") :: dir :: rem ->
@@ -280,10 +281,10 @@ let parse () =
 	Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
 	Cdglobals.set_utf8 (); parse_rec rem
-
+	  
     | ("-q" | "-quiet" | "--quiet") :: rem ->
 	quiet := true; parse_rec rem
-
+	  
     | ("-h" | "-help" | "-?" | "--help") :: rem ->
 	banner (); usage ()
     | ("-v" | "-version" | "--version") :: _ ->
@@ -317,13 +318,17 @@ let parse () =
 	Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
+    | ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
+	Cdglobals.coqlib_path := d; parse_rec rem
+    | ("--coqlib_path" | "-coqlib_path") :: [] ->
+	usage ()
     | f :: rem -> 
 	add_file (what_file f); parse_rec rem
   in 
-  parse_rec (List.tl (Array.to_list Sys.argv));
-  List.rev !files
-
+    parse_rec (List.tl (Array.to_list Sys.argv));
+    List.rev !files
 
+      
 (*s The following function produces the output. The default output is
     the \LaTeX\ document: in that case, we just call [Web.produce_document]. 
     If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
@@ -331,41 +336,41 @@ let parse () =
 
 let locally dir f x =
   let cwd = Sys.getcwd () in
-  try
-    Sys.chdir dir; let y = f x in Sys.chdir cwd; y
-  with e ->
-    Sys.chdir cwd; raise e
+    try
+      Sys.chdir dir; let y = f x in Sys.chdir cwd; y
+    with e ->
+      Sys.chdir cwd; raise e
 
 let clean_temp_files basefile =
   let remove f = try Sys.remove f with _ -> () in
-  remove (basefile ^ ".tex");
-  remove (basefile ^ ".log");
-  remove (basefile ^ ".aux");
-  remove (basefile ^ ".dvi");
-  remove (basefile ^ ".ps");
-  remove (basefile ^ ".haux");
-  remove (basefile ^ ".html")
-
+    remove (basefile ^ ".tex");
+    remove (basefile ^ ".log");
+    remove (basefile ^ ".aux");
+    remove (basefile ^ ".dvi");
+    remove (basefile ^ ".ps");
+    remove (basefile ^ ".haux");
+    remove (basefile ^ ".html")
+      
 let clean_and_exit file res = clean_temp_files file; exit res
-
+  
 let cat file =
   let c = open_in file in
-  try
-    while true do print_char (input_char c) done
-  with End_of_file ->
-    close_in c
+    try
+      while true do print_char (input_char c) done
+    with End_of_file ->
+      close_in c
 
 let copy src dst =
   let cin = open_in src 
   and cout = open_out dst in
-  try
-    while true do Pervasives.output_char cout (input_char cin) done
-  with End_of_file ->
-    close_in cin; close_out cout
+    try
+      while true do Pervasives.output_char cout (input_char cin) done
+    with End_of_file ->
+      close_in cin; close_out cout
 
 
 (*s Functions for generating output files *)
-
+	
 let gen_one_file l =
   let file = function
     | Vernac_file (f,m) -> 
@@ -416,15 +421,15 @@ let gen_mult_files l =
 let index_module = function
   | Vernac_file (_,m) -> Index.add_module m
   | Latex_file _ -> ()
-
+      
 let produce_document l =
   List.iter index_module l;
   (if !target_language=HTML then
-    let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.css") in
+    let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
     let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
       copy src dst);
   (if !target_language=LaTeX then
-    let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.sty") in
+    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
@@ -439,7 +444,7 @@ let produce_document l =
 	close_out_file()
     | MultFiles ->
 	gen_mult_files l
-
+	  
 let produce_output fl =
   if not (!dvi || !ps) then begin
     produce_document fl
@@ -493,7 +498,7 @@ let produce_output fl =
 
 let main () =
   let files = parse () in
-  if not !quiet then banner ();
-  if files <> [] then produce_output files
-
+    if not !quiet then banner ();
+    if files <> [] then produce_output files
+      
 let _ = Printexc.catch main ()
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 4c4cf5ec..e6a0a72b 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 8669 2006-03-28 17:34:15Z notin $ i*)
+(*i $Id: output.ml 8863 2006-05-26 10:33:21Z notin $ i*)
 
 open Cdglobals
 open Index
@@ -336,12 +336,12 @@ module Html = struct
 	raw_ident s
     i*)
 
-  let ident_ref m s = match find_module m with
+  let ident_ref m fid s = match find_module m with
     | Local ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
     | Coqlib when !externals ->
 	let m = Filename.concat !coqlib m in
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
     | Coqlib | Unknown ->
 	raw_ident s
 
@@ -351,18 +351,20 @@ module Html = struct
       raw_ident s; 
       printf "</span>"
     end else 
-      try
-	(match Index.find !current_module loc with
-	   | Def _ -> 
-	       printf "<a name=\"%s\"></a>" s; raw_ident s
-           | Mod (m,s') when s = s' ->
-	       module_ref m s
-	   | Ref (m,s') when s = s' -> 
-	       ident_ref m s
-	   | Mod _ | Ref _ ->
-	       raw_ident s)
-      with Not_found ->
-	raw_ident s
+      begin
+	try
+	  (match Index.find !current_module loc with
+	     | Def (fullid,_) -> 
+		 printf "<a name=\"%s\"></a>" fullid; raw_ident s
+             | Mod (m,s') when s = s' ->
+		 module_ref m s
+	     | Ref (m,fullid) -> 
+		 ident_ref m fullid s
+	     | Mod _ | Ref _ ->
+		 raw_ident s)
+	with Not_found ->
+	  raw_ident s
+      end
 	  
   let with_html_printing f tok =
     try 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index ad9057ad..5c6c7952 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 8666 2006-03-27 17:02:49Z notin $ i*)
+(*i $Id: pretty.mll 8861 2006-05-24 15:52:15Z notin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -173,8 +173,11 @@ let firstchar =
   (* utf-8 letterlike symbols *) 
   '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
 let identchar = 
-  firstchar | ['\'' '0'-'9' '@']
-let identifier = firstchar identchar*
+  firstchar | ['\'' '0'-'9' '@' ]
+let id = firstchar identchar*
+let pfx_id = (id '.')*
+let identifier = 
+  id | pfx_id id
 
 let symbolchar_no_brackets =
   ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#'