diff options
| author | Gaëtan Gilbert | 2017-08-31 16:02:00 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-03 13:36:05 +0200 |
| commit | ebfefb3dbea6770df1e860b5852e59d6852d161f (patch) | |
| tree | a282fede2d593aa41026624d2b28430c2b8d2788 /tools/coqdoc/output.ml | |
| parent | b1b89157a7ab59278db1fed77f41cab2aa2d3a9f (diff) | |
coqdoc Index.find_string: remove unused argument.
Unused since 6832c60f741e6bfb2a850d567fd6a1dff7059393.
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d252270021..c640167ac8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -431,7 +431,7 @@ module Latex = struct else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then try - let tag = Index.find_string (get_module false) s in + let tag = Index.find_string s in reference (translate s) tag with _ -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s @@ -706,7 +706,7 @@ module Html = struct else if is_keyword s then printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then - try reference (translate s) (Index.find_string (get_module false) s) + try reference (translate s) (Index.find_string s) with Not_found -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s |