| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-08 | Convert 2nd part of rewriting chapter to prodn | Jim Fehrle | |
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle | |
| 2020-11-24 | Convert auto chapter to prodn | Jim Fehrle | |
| 2020-11-09 | [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. | Théo Zimmermann | |
| The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version. | |||
| 2020-10-20 | Add some missing smallcaps. | Théo Zimmermann | |
| 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 |