diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-11-20 18:43:31 +0100 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2017-11-22 11:14:46 +0100 |
| commit | 2db70092d63065be8a5902764e0d1d5f1ea01e6c (patch) | |
| tree | 478c124734b6444141378a1df22488f77b2102c7 /kernel/kernel.mllib | |
| parent | 2a857da2a88855a6c9f0fa7e48a8700c1613e0c7 (diff) | |
Fix universe polymorphic Program obligations.
The universes of the obligations should all be non-algebraic as they
might appear in instances of other obligations and instances only take
non-algebraic universes as arguments.
Diffstat (limited to 'kernel/kernel.mllib')
0 files changed, 0 insertions, 0 deletions