From f5be988da566d0a48c67bd81be6d32376b3ba2a5 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 13 Feb 2020 18:47:42 +0100 Subject: [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 --- doc/sphinx/language/extensions/index.rst | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 doc/sphinx/language/extensions/index.rst (limited to 'doc/sphinx/language/extensions') diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst new file mode 100644 index 0000000000..5b5c2ab737 --- /dev/null +++ b/doc/sphinx/language/extensions/index.rst @@ -0,0 +1,28 @@ +.. _extensions: + +=================== +Language extensions +=================== + +Elaboration extends the language accepted by the Coq kernel to make it +easier to use. For example, this lets the user omit most type +annotations because they can be inferred, call functions with implicit +arguments which will be inferred as well, extend the syntax with +notations, factorize branches when pattern-matching, etc. In this +chapter, we present these language extensions and we give some +explanations on how this language is translated down to the core +language presented in the :ref:`previous chapter `. + +This chapter is divided in several sub-chapters: + +.. toctree:: + :maxdepth: 1 + + ../gallina-extensions + ../../addendum/extended-pattern-matching + ../../user-extensions/syntax-extensions + ../../addendum/implicit-coercions + ../../addendum/type-classes + ../../addendum/canonical-structures + ../../addendum/program + ../../proof-engine/vernacular-commands -- cgit v1.2.3 From 1be31dea4cfd31522898edc07fee0829fea7c68d Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 19 Mar 2020 15:51:18 +0100 Subject: Adapt to sub-TOC not showing in PDF output. --- doc/sphinx/language/extensions/index.rst | 2 -- 1 file changed, 2 deletions(-) (limited to 'doc/sphinx/language/extensions') diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst index 5b5c2ab737..f22927d627 100644 --- a/doc/sphinx/language/extensions/index.rst +++ b/doc/sphinx/language/extensions/index.rst @@ -13,8 +13,6 @@ chapter, we present these language extensions and we give some explanations on how this language is translated down to the core language presented in the :ref:`previous chapter `. -This chapter is divided in several sub-chapters: - .. toctree:: :maxdepth: 1 -- cgit v1.2.3