diff options
| author | Théo Zimmermann | 2020-02-13 18:47:42 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-19 15:51:22 +0100 |
| commit | f5be988da566d0a48c67bd81be6d32376b3ba2a5 (patch) | |
| tree | 44e5adff3d2f3802f80dfda3fc5dfb8609dfe6fe /doc/sphinx/appendix | |
| parent | 918e301faa228190f885f860510f4b6c352620f5 (diff) | |
[refman] Move chapters into new structure.
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>
Diffstat (limited to 'doc/sphinx/appendix')
| -rw-r--r-- | doc/sphinx/appendix/history-and-changes/index.rst | 20 | ||||
| -rw-r--r-- | doc/sphinx/appendix/indexes/index.rst | 24 |
2 files changed, 44 insertions, 0 deletions
diff --git a/doc/sphinx/appendix/history-and-changes/index.rst b/doc/sphinx/appendix/history-and-changes/index.rst new file mode 100644 index 0000000000..3535a4d8a7 --- /dev/null +++ b/doc/sphinx/appendix/history-and-changes/index.rst @@ -0,0 +1,20 @@ +.. _history-and-changes: + +========================== +History and recent changes +========================== + +This chapter is divided in two parts. The first one is about the +early history of Coq and is presented in chronological order. The +second one provides release notes about recent versions of Coq and is +presented in reverse chronological order. When updating your copy of +Coq to a new version (especially a new major version), it is strongly +recommended that you read the corresponding release notes. They may +contain advice that will help you understand the differences with the +previous version and upgrade your projects. + +.. toctree:: + :maxdepth: 1 + + ../../history + ../../changes diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst new file mode 100644 index 0000000000..a5032ff822 --- /dev/null +++ b/doc/sphinx/appendix/indexes/index.rst @@ -0,0 +1,24 @@ +:orphan: + +.. _indexes: + +======== +Indexes +======== + +We provide various specialized indexes that are helpful to quickly +find what you are looking for. + +.. toctree:: + + ../../genindex + ../../coq-cmdindex + ../../coq-tacindex + ../../coq-optindex + ../../coq-exnindex + +For reference, here are direct links to the documentation of: + +- :ref:`flags, options and tables <flags-options-tables>`; +- controlling the display of warning messages with the :opt:`Warnings` + option. |
