diff options
| author | Tej Chajed | 2018-01-25 15:37:43 -0500 |
|---|---|---|
| committer | Tej Chajed | 2018-01-26 10:43:05 -0500 |
| commit | 885307fc52e02d98c48851d0a07e8f9b64d975b0 (patch) | |
| tree | 4ce8fdd91762b2b5cf5a20edaac31c384e7730dd /kernel/type_errors.mli | |
| parent | 35a275e22b72abba344b837e7276af8057d5da2c (diff) | |
Support universe instances on the literal Type
Fixes BZ#5726.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions