aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-08-31 16:02:00 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-07-03 13:36:05 +0200
commitebfefb3dbea6770df1e860b5852e59d6852d161f (patch)
treea282fede2d593aa41026624d2b28430c2b8d2788 /tools/coqdoc
parentb1b89157a7ab59278db1fed77f41cab2aa2d3a9f (diff)
coqdoc Index.find_string: remove unused argument.
Diffstat (limited to 'tools/coqdoc')
-rw-r--r--tools/coqdoc/index.ml2
-rw-r--r--tools/coqdoc/index.mli2
-rw-r--r--tools/coqdoc/output.ml4
3 files changed, 4 insertions, 4 deletions
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index df493fdf7..885324aa0 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -77,7 +77,7 @@ let add_ref m loc m' sp id ty =
let find m l = Hashtbl.find reftable (m, l)
-let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
+let find_string s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
(* Coq modules *)
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 5cd301389..7c9aad67f 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -41,7 +41,7 @@ type index_entry =
val find : coq_module -> loc -> index_entry
(* Find what data is referred to by some string in some coq module *)
-val find_string : coq_module -> string -> index_entry
+val find_string : string -> index_entry
val add_module : coq_module -> unit
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index d25227002..c640167ac 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