From 6832c60f741e6bfb2a850d567fd6a1dff7059393 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 3 Oct 2008 14:41:08 +0000
Subject: Minor fixes related to coqdoc and --interpolate and the dependent
 induction test-suite script.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11426 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coqdoc/index.mll | 10 ++++++----
 tools/coqdoc/output.ml |  4 ++--
 2 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 5b54255904..b41c19ac3f 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -66,18 +66,20 @@ let full_ident sp id =
     
 let add_def loc ty sp id = 
   Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty));
-  Hashtbl.add deftable (!current_library, id) (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 = 
-  Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty))
+  if Hashtbl.mem reftable (m, loc) then ()
+  else
+    Hashtbl.add reftable (m, loc) (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, id) (Mod (m', id))
+  Hashtbl.add deftable id (Mod (m', id))
     
 let find m l = Hashtbl.find reftable (m, l)
   
-let find_string m s = Hashtbl.find deftable (m, s)
+let find_string m s = Hashtbl.find deftable s
   
 (*s Manipulating path prefixes *) 
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index a7ed7444a0..2d547af798 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -273,8 +273,8 @@ module Latex = struct
 	  end else begin
 	    if !Cdglobals.interpolate then
 	      try reference s (Index.find_string !current_module s)
-	      with _ -> printf "\\coqdocvar{"; raw_ident s; printf "}" 
-	    else printf "\\coqdocvar{"; raw_ident s; printf "}"
+	      with _ -> printf "\\coqdocvar{"; raw_ident s; printf "}"
+	    else (printf "\\coqdocvar{"; raw_ident s; printf "}")
 	  end
       end
     end
-- 
cgit v1.2.3