| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Sanitize universe declaration in Context (stop using a ref...) |  Gaëtan Gilbert | 2018-03-05 |
| When there is more than one variable to declare we stop trying to attach global universes (ie monomorphic or section polymorphic) to one of them. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |