diff options
| author | Théo Zimmermann | 2019-02-06 15:37:07 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-06 15:37:07 +0100 |
| commit | 177a438806f811901ad0aeab4ed69014e9d2af26 (patch) | |
| tree | 5331e522a6c69fda7731150b8c068c3fc9b4e6e6 /kernel/nativecode.ml | |
| parent | c1123f1c05943b8d09245b8fa9d90664344c054d (diff) | |
| parent | 162101e6bc5b3bb33b741ff51e37805ffd624d0d (diff) | |
Merge PR #9456: The lowest universe level is 1.
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions