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 /lib/util.ml | |
| parent | b1b89157a7ab59278db1fed77f41cab2aa2d3a9f (diff) | |
coqdoc Index.find_string: remove unused argument.
Unused since 6832c60f741e6bfb2a850d567fd6a1dff7059393.
Diffstat (limited to 'lib/util.ml')
0 files changed, 0 insertions, 0 deletions