diff options
| author | Gaëtan Gilbert | 2018-08-28 15:21:12 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 15:05:57 +0200 |
| commit | ec4aa4971f7789eeccec2f38f2bb7ec976f87ede (patch) | |
| tree | dcb629e86ab9e7ee35ff5dcdd2d4e8ce085a597b /kernel/nativecode.ml | |
| parent | b5c9a9678b2a189edf092f4b8dbebccd49430154 (diff) | |
Do not catch already declared universes in Environ.add_universes
Include is still causing repeat declarations in add_universes_set
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions