Include all menu entries in the menu/short TOC so that users can view

menu options for all chapters without having to load a new chapter. Change "Introcution" title to "Introduction and Contents"
SkySkimmer · Oct 10, 2018 · 7489829 · 7489829
1 parent 3a0a9c2
commit 7489829
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 8 deletions.
diff --git a/Makefile.doc b/Makefile.doc
@@ -10,7 +10,7 @@
 
 # Makefile for the Coq documentation
 
-# Read INSTALL.doc to learn about the dependencies
+# Read doc/README.md to learn about the dependencies
 
 # The main entry point :
 

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
@@ -193,8 +193,9 @@ def setup(app):
 # Theme options are theme-specific and customize the look and feel of a theme
 # further.  For a list of options available for each theme, see the
 # documentation.
-#html_theme_options = {}
-
+html_theme_options = {
+    'collapse_navigation': False
+}
 html_context = {
     'display_github': True,
     'github_user': 'coq',

diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
@@ -1,13 +1,13 @@
 .. _introduction:
 
 ==========================
-Introduction
+Introduction and Contents
 ==========================
 
 .. include:: introduction.rst
 
-Table of contents
------------------
+Contents
+--------
 
 .. toctree::
    :caption: Indexes

diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
@@ -44,7 +44,7 @@ are processed from a file.
 .. seealso:: :ref:`thecoqcommands`.
 
 How to read this book
-=====================
+---------------------
 
 This is a Reference Manual, so it is not intended for continuous reading.
 We recommend using the various indexes to quickly locate the documentation
@@ -90,7 +90,7 @@ Nonetheless, the manual has some structure that is explained below.
    solvers and tactics. See the table of contents for a complete list.
 
 List of additional documentation
-================================
+--------------------------------
 
 This manual does not contain all the documentation the user may need
 about |Coq|. Various informations can be found in the following documents: