diff options
| author | Gaëtan Gilbert | 2018-08-28 15:20:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 15:05:57 +0200 |
| commit | b5c9a9678b2a189edf092f4b8dbebccd49430154 (patch) | |
| tree | edc940c403b3c7ed79e733bb5f62beb39216398e /kernel/nativelib.ml | |
| parent | cc66d4a0977db4994000bfc7e45937b3ccff3c93 (diff) | |
Avoid repeat univ declaration in cumulative subtyping check
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions