From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 tools/coqdoc/output.ml | 34 ++++++++++++++++++----------------
 1 file changed, 18 insertions(+), 16 deletions(-)

(limited to 'tools/coqdoc/output.ml')

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 
-- 
cgit v1.2.3