Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisation (add_glob* et dump_*)

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

1 files changed, 8 insertions, 10 deletions

diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 0522bbac0..a75b7196d 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -417,17 +417,14 @@ module Html = struct
   let stop_verbatim () = printf "</pre>\n"
 
   let module_ref m s = 
-    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    (*i
     match find_module m with
-    | Local ->
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | Coqlib when !externals ->
-	let m = Filename.concat !coqlib m in
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | Coqlib | Unknown ->
-	raw_ident s
-    i*)
+      | Local ->
+	  printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
+      | Coqlib when !externals ->
+	  let m = Filename.concat !coqlib m in
+	    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
+      | Coqlib | Unknown ->
+	  raw_ident s
 
   let ident_ref m fid s = 
     match find_module m with
@@ -446,6 +443,7 @@ module Html = struct
       printf "</span>"
     end else 
       begin
+	Printf.eprintf "DEBUG: looking for (%s, %d)\n" !current_module loc;
 	try
 	  (match Index.find !current_module loc with
 	     | Def (fullid,_) ->