aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/appendix
diff options
context:
space:
mode:
authorThéo Zimmermann2020-02-13 18:47:42 +0100
committerThéo Zimmermann2020-03-19 15:51:22 +0100
commitf5be988da566d0a48c67bd81be6d32376b3ba2a5 (patch)
tree44e5adff3d2f3802f80dfda3fc5dfb8609dfe6fe /doc/sphinx/appendix
parent918e301faa228190f885f860510f4b6c352620f5 (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.rst20
-rw-r--r--doc/sphinx/appendix/indexes/index.rst24
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.