diff options
author | 2017-02-22 02:08:29 +0100 | |
---|---|---|
committer | 2017-04-12 16:49:46 +0200 | |
commit | 46856a80958f1aaa3242b6d37f018df9528e5e5f (patch) | |
tree | 3c15b53a6f6ff36629e7fbff317ee73cc9ed818f /lib/flags.mli | |
parent | ce2b2058587224ade9261cd4127ef4f6e94d356b (diff) |
[vernac] vernacentries.mli cleanup
This header file had accumulated quite a bit of cruft over the
years, we clean it up while we are at it.
No functional change as all the removed variables/methods were noops
long time ago.
Diffstat (limited to 'lib/flags.mli')
0 files changed, 0 insertions, 0 deletions