diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-28 12:06:24 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-28 13:58:37 +0200 |
| commit | e260172f03f792a388797f066438e079290074d0 (patch) | |
| tree | 9d662af2cbd8e9b27f441cdb664dd22a61e52de8 /tools/coqdoc/output.ml | |
| parent | 49162693b37a3bebc47cd6f667b2e7ebea209fc6 (diff) | |
Remove unused lookup table.
Diffstat (limited to 'tools/coqdoc/output.ml')
0 files changed, 0 insertions, 0 deletions