| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix #6323: stronger restrict universe context vs abstract. |  Gaëtan Gilbert | 2017-12-06 |
| In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c]. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |