aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorHugo Herbelin2016-10-11 12:58:42 +0200
committerHugo Herbelin2016-10-17 20:14:13 +0200
commit4e31561f7e0d5e647e86978806cae82ffb35f90b (patch)
treeca7f7540c690bd40c5e29fcd3c8cde7c257ff9a6 /kernel
parente4fcf8f9af193f125eb6ee101e739ba4460bd8b8 (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')
0 files changed, 0 insertions, 0 deletions