diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/index.mll | 10 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 4 |
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 |