aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-09-29 18:20:36 +0200
committerEmilio Jesus Gallego Arias2018-09-30 14:25:26 +0200
commite5b3bd6b12af9f08d7913e25748fba9c4f9fd48f (patch)
tree500c76251fd9973e18bd1840839983d9f36b2d71 /kernel/nativecode.mli
parent081326a7b2c64e8620777aeae7e2275144b65b4b (diff)
[api] Cleanup `Decls`: remove unused function, move vernac helper.
It seems these two functions don't belong there. We can remove one, and place the other actually next to whether their semantics are necessary. Note that indeed the whole `Decls` file seems a bit suspicious, why we do we register this information in a separate table instead of in the main ones in `Lib` ? At the suggestion of Gaƫtan Gilbert we also remove unused function `is_instance`.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions