diff options
| author | Matthieu Sozeau | 2015-01-18 00:07:32 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:07:32 +0530 |
| commit | 5e5d51762df0e34769225e8c59c77b97b1212c29 (patch) | |
| tree | 61aa0a74d77089ed4a7db12ff6fc46059ab2fb61 /kernel/nativecode.ml | |
| parent | 9d8347abc07dec1edd804b2fa39db40088b5cf3d (diff) | |
There was one more universe needed due to the use of now non-universe-polymorphic
ID, fixing the script results in 3 universes for the stdlib again.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions