diff options
| author | Gaëtan Gilbert | 2018-10-30 17:45:17 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-30 21:46:57 +0100 |
| commit | 25df997df4b5b6882f8bf316c5cfb8145ba5f08d (patch) | |
| tree | f71871a0b50530429b95cecc962cd89d2420dce3 /kernel/typeops.mli | |
| parent | d32301dde8071acc914286c675b9749e27f368d2 (diff) | |
Simplify universe handling in environ constant_type functions
Diffstat (limited to 'kernel/typeops.mli')
0 files changed, 0 insertions, 0 deletions