From edd0ede5ac057f6a7296351f608f162cd8b0a32b Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 25 Sep 2018 12:46:08 +0200
Subject: Fix title of Introduction chapter in HTML version.

And location of footnote.
---
 doc/sphinx/index.html.rst   | 12 +++++++-----
 doc/sphinx/index.latex.rst  |  5 +++++
 doc/sphinx/introduction.rst |  5 -----
 3 files changed, 12 insertions(+), 10 deletions(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index da129a3ed0..cf12b57414 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -1,11 +1,8 @@
-==========================
- The Coq Reference Manual
-==========================
-
 .. _introduction:
 
+==========================
 Introduction
-------------
+==========================
 
 .. include:: introduction.rst
 
@@ -89,3 +86,8 @@ License
 -------
 
 .. include:: license.rst
+
+.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
+   Optionally, you can enhance it with the minor mode
+   Company-Coq :cite:`Pit16`
+   (see https://github.com/cpitclaudel/company-coq).
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index 13bc1a19e7..af757f8746 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -7,6 +7,11 @@ Introduction
 
 .. include:: introduction.rst
 
+.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
+   Optionally, you can enhance it with the minor mode
+   Company-Coq :cite:`Pit16`
+   (see https://github.com/cpitclaudel/company-coq).
+
 Credits
 -------
 
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index b8d2f6b6dc..5bb7bf542c 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -35,11 +35,6 @@ are processed from a file.
    The `coqtop` read-eval-print-loop can also be used directly, for debugging
    purposes.
 
-   .. [#PG] Proof-General is available at https://proofgeneral.github.io/.
-      Optionally, you can enhance it with the minor mode
-      Company-Coq :cite:`Pit16`
-      (see https://github.com/cpitclaudel/company-coq).
-
 -  The compiled mode acts as a proof checker taking a file containing a
    whole development in order to ensure its correctness. Moreover,
    |Coq|’s compiler provides an output file containing a compact
-- 
cgit v1.2.3