diff options
| author | Pierre-Marie Pédrot | 2017-07-19 14:05:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-26 15:12:47 +0200 |
| commit | 906b48ff401f22be6059a6cdde8723b858102690 (patch) | |
| tree | 0254ba66d050474ff0507dc0302d1da3b0d40024 /kernel/declarations.ml | |
| parent | 665256fec8465ff0adb943063c25f07a6ca54618 (diff) | |
Avoiding a variable shadowing in the kernel.
This ought to ease the understanding of the code.
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions