diff options
| author | Gaëtan Gilbert | 2019-01-30 12:59:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-30 13:01:55 +0100 |
| commit | f7148d56b17ee7d06cac26392c85f3b8c7cbd974 (patch) | |
| tree | 9c9dc8427d4e4ccf766d941efa1e80b217f89b1c /kernel/type_errors.mli | |
| parent | a9b141469fe3036355be95d8cf5f0bf5c240fe37 (diff) | |
Cleanup universe length for inductives in vconv
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions