| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-04-07 | Support universe bindings and universe constraints in Let definitions. | Théo Zimmermann | |
| Let vs Definition / Example syntax was split in 7c28130 for parsing reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could be introduced. This split is probably the reason why Let was overlooked when support for universe bindings and universe constraints were added to Definition and variants. | |||
| 2020-04-03 | Move section on sections in appropriate location (inside core). | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |