diff options
| author | Emilio Jesus Gallego Arias | 2017-02-22 02:08:29 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-12 16:49:46 +0200 |
| commit | 46856a80958f1aaa3242b6d37f018df9528e5e5f (patch) | |
| tree | 3c15b53a6f6ff36629e7fbff317ee73cc9ed818f /lib/flags.ml | |
| 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.ml')
0 files changed, 0 insertions, 0 deletions