diff options
| author | Hugo Herbelin | 2017-03-09 13:50:22 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-09 15:40:20 +0100 |
| commit | b7415c84269b1553470216b06871def933e2f3bd (patch) | |
| tree | 15c640670945dde7a431e622004e3a1fb1bdc0ee /kernel/nativecode.mli | |
| parent | 76fc1698fbb6b523c5c0d15f0b15a2d035649496 (diff) | |
Clarifying doc about interpretation of scopes in notations (#5386).
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions