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

2 files changed, 8 insertions, 6 deletions

diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 5b5425590..b41c19ac3 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 a7ed7444a..2d547af79 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