| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-20 | Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clauses | Pierre-Marie Pédrot | |
| Reviewed-by: jfehrle Reviewed-by: ppedrot | |||
| 2020-11-18 | Use only nats for occs_nums rather than ints | Jim Fehrle | |
| 2020-11-17 | Fixes #13235: remove fragile tolerance for degenerate in-hyps clause. | Hugo Herbelin | |
| Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com> | |||
| 2020-11-16 | Merge PR #13384: Warn on hints without an explicit locality | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 | |||
| 2020-11-16 | Merge PR #12516: Deprecate `Grab Existential Variables` and `Existential` ↵ | Pierre-Marie Pédrot | |
| commands Reviewed-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2020-11-16 | Document the deprecation of the commands. | Pierre-Marie Pédrot | |
| 2020-11-16 | Document the new warning. | Pierre-Marie Pédrot | |
| 2020-11-16 | Tentative fix for the refman. | Pierre-Marie Pédrot | |
| 2020-11-15 | Document the new export locality for the remaining hint commands. | Pierre-Marie Pédrot | |
| 2020-11-10 | Convert logic.rst 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-11-05 | Improve title of first proof chapter. | Théo Zimmermann | |
| 2020-11-05 | Change the title of the automatic tactic chapter and of its sections. | Théo Zimmermann | |
| Prefer the term 'solver' to 'decision procedure'. | |||
| 2020-11-05 | Add new sections to automatic tactic chapter. | Théo Zimmermann | |
| 2020-11-05 | Various fixes. | Théo Zimmermann | |
| 2020-11-05 | Merge content from two origins into the same file. | Théo Zimmermann | |
| 2020-11-05 | Move proof handling chapter in new location. | Théo Zimmermann | |
| 2020-11-05 | Octopus merge to preserve history of content split over multiple files. | Théo Zimmermann | |
| 2020-11-05 | Remove everything before goal management. | Théo Zimmermann | |
| 2020-11-05 | Remove everything after the content on goal management. | Théo Zimmermann | |
| 2020-11-05 | Move some content on goal management to the proof mode page. | Théo Zimmermann | |
| 2020-11-05 | Keep only the content on solvers for logic and equality. | Théo Zimmermann | |
| 2020-11-05 | Move some content to a new page on solvers for logic and equality. | Théo Zimmermann | |
| 2020-11-05 | Keep only content about auto. | Théo Zimmermann | |
| 2020-11-05 | Move some content to a new page on automation. | Théo Zimmermann | |
| 2020-11-05 | Add new page to writing proof index. | Théo Zimmermann | |
| 2020-11-05 | Remove everything before term rewriting and simplification. | Théo Zimmermann | |
| 2020-11-05 | Remove everything after term rewriting and simplification. | Théo Zimmermann | |
| 2020-11-05 | Move some content to a new page on term rewriting and simplification. | Théo Zimmermann | |
| 2020-10-20 | Add some missing smallcaps. | 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 |