diff options
| author | Hugo Herbelin | 2016-10-11 12:58:42 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-17 20:14:13 +0200 |
| commit | 4e31561f7e0d5e647e86978806cae82ffb35f90b (patch) | |
| tree | ca7f7540c690bd40c5e29fcd3c8cde7c257ff9a6 /kernel/nativecode.ml | |
| parent | e4fcf8f9af193f125eb6ee101e739ba4460bd8b8 (diff) | |
Removing export of location_table outside of cLexer.
It was not used any more by coqdoc since b8194b22 (Dec 2010).
The table is now only part of the lexer function closure
(and only in the camlp5 case).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions