| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann | |
| Add headers to a few files which were missing them. | |||
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann | |
| 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 |