diff options
| author | Matthieu Sozeau | 2014-06-17 11:18:10 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-17 15:42:14 +0200 |
| commit | b8834d66013b38cef247507f312bb081de04da27 (patch) | |
| tree | 13bf7e5c58c160eac0dafa6d36e9f7a9ad6745e9 /kernel/inductive.ml | |
| parent | 0091c528cb1b0171215a6ef5a47f26763a4edc09 (diff) | |
Existing Class now works with universe polymorphism. Fixes HoTT bug #063
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions