diff options
| author | Gaëtan Gilbert | 2020-01-30 23:40:08 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-30 23:40:08 +0100 |
| commit | c20fe3443f905dfea3ff746407cd1649ed8867ff (patch) | |
| tree | fb25530b54fa53a16636c587863e56ccf5865251 /kernel/safe_typing.ml | |
| parent | a7af2f6571d007b6f83a1ec9252b52f69907a965 (diff) | |
Factorize export_private_constants + register_side_effect
Diffstat (limited to 'kernel/safe_typing.ml')
0 files changed, 0 insertions, 0 deletions