| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-07 | Avoid trivial (u=u) constraints in AcyclicGraph.constraints_for | Gaëtan Gilbert | |
| Not sure how often this happens in practice but it seems it could. | |||
| 2018-12-17 | Remove universe specific terminology from acyclicgraph | Gaëtan Gilbert | |
| This means removing [univ], [level] and derived abbreviations like [lvl]. We keep using u, v for variable names as doing otherwise would be too intrusive, and it's not overly universe specific. | |||
| 2018-12-17 | Make ugraph implementation abstract wrt universe specifics | Gaëtan Gilbert | |
| This should give better visibility of universe specific operations vs generic graph operations. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |