aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2016-07-20 12:29:13 +0200
committerMatthieu Sozeau2016-07-20 12:30:01 +0200
commit21f7472e430917707ff02930a05e13251e1fff9d (patch)
tree39c45c0117299add5e9d88ecc65782c4621fe7b4 /kernel/nativecode.mli
parent522bcd72a567a3ae29162519a9a9736581367251 (diff)
Fix bug #4780: universe leak in letin_tac
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions