| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-06-08 | Convert Ltac chapter to prodn | Jim Fehrle | |
| 2020-05-16 | Merge PR #8855: More search options | Emilio Jesus Gallego Arias | |
| Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: kyoDralliam | |||
| 2020-05-15 | Document new Search features. | Théo Zimmermann | |
| 2020-05-15 | Fix typo. | Théo Zimmermann | |
| 2020-05-14 | Fix title level and a build failure. | Théo Zimmermann | |
| 2020-05-14 | Add some markers of origin. | Théo Zimmermann | |
| 2020-05-14 | Reintroduce leftover parts; update index files; small fixes. | Théo Zimmermann | |
| 2020-05-14 | Refactoring of the first part of the reference manual. | Théo Zimmermann | |
| 2020-05-14 | Preserve Implicit arguments file. | Théo Zimmermann | |
| 2020-05-14 | Remove Canonical structures from Implicit arguments. | Théo Zimmermann | |
| 2020-05-14 | Merge doc on Canonical structures from two origins. | Théo Zimmermann | |
| 2020-05-14 | Move Canonical structures file into new location. | Théo Zimmermann | |
| 2020-05-14 | Add Canonical structure declarations to Canonical structures file. | Théo Zimmermann | |
| 2020-05-14 | Extract Canonical structures from Implicit arguments. | Théo Zimmermann | |
| 2020-05-14 | Split Gallina extensions into multiple files. | Théo Zimmermann | |
| 2020-05-14 | Merge doc on extended pattern matching from two origins. | Théo Zimmermann | |
| 2020-05-14 | Move extended pattern matching to new location. | Théo Zimmermann | |
| 2020-05-13 | Add section on pattern matching from Gallina ext. | Théo Zimmermann | |
| 2020-05-13 | New file on existential variables. | Théo Zimmermann | |
| 2020-05-01 | Move essential vocabulary and syntax conventions to section on basics. | Théo Zimmermann | |
| 2020-04-26 | Convert syntax extensions chapter to prodn | Jim Fehrle | |
| 2020-04-10 | Convert vernac commands chapter to prodn, update syntax | Jim Fehrle | |
| 2020-04-03 | Move section on implicit arguments in appropriate location (inside extensions). | Théo Zimmermann | |
| 2020-03-19 | Adapt to sub-TOC not showing in PDF output. | Théo Zimmermann | |
| 2020-03-19 | [refman] Move chapters into new structure. | Théo Zimmermann | |
| As a first step toward a deeper refactoring of the reference manual, we move existing chapters into a new structure. We use the Sphinx support for top-level chapters spanning multiple pages to consolidate existing chapters into a smaller number of chapters and a smaller number of parts. Now the full top-level table of content can be seen in one glance. Most of the new chapters are divided into several sub-chapters (on separate pages) that correspond to the pre-existing chapters. These new top-level chapters gathering several chapters together have gained a new introduction. The main introduction has been rewritten / simplified as well. For now, the URL of pre-existing chapters does not change. The intent is to further refactor the manual by splitting some of these sub-chapters into smaller ones, and by moving things around. While the sub-chapters are likely to evolve very much in the future, the top-level table of content is almost final (except that the "Using Coq" part may gain one or two additional chapters on proof engineering / project management). Thanks to Jim Fehrle for investigating how to split a chapter on multiple pages and to both Jim and Matthieu Sozeau for the discussion that led to this new structure. See also the related CEP: https://github.com/coq/ceps/pull/43 Additional notes: - A new directory structure has been created reflecting the new chapter structure. - The indexes chapter has been removed from the PDF version since it wasn't working. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net> | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |