diff options
| author | Hugo Herbelin | 2018-10-19 23:34:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 23:34:24 +0200 |
| commit | 02f7b4ac1968ca4522d144e34b52dead3871a8b7 (patch) | |
| tree | 1e649e34972959b77eeebd4c5c6237fd12af1f61 /kernel/nativecode.ml | |
| parent | 3799939088b5aa616974a0d37de7e2616024f222 (diff) | |
| parent | 4ac1e342fe420e0b3f3adc9e619d2e98eba2111d (diff) | |
Merge PR #8758: [api] Qualify access to `Nametab`
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions