diff options
author | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-31 16:02:00 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-03 13:36:05 +0200 |
commit | ebfefb3dbea6770df1e860b5852e59d6852d161f (patch) | |
tree | a282fede2d593aa41026624d2b28430c2b8d2788 /tools/coqdoc/index.ml | |
parent | b1b89157a7ab59278db1fed77f41cab2aa2d3a9f (diff) |
coqdoc Index.find_string: remove unused argument.
Unused since 6832c60f741e6bfb2a850d567fd6a1dff7059393.
Diffstat (limited to 'tools/coqdoc/index.ml')
-rw-r--r-- | tools/coqdoc/index.ml | 2 |
1 files changed, 1 insertions, 1 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 *) |