Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix universe polymorphic Program obligations. | Matthieu Sozeau | 2017-11-22 |
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. |