From 81e55a33d518aa70cef62af3cdf3d6a013960ac6 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Mon, 13 Aug 2018 17:44:36 -0400
Subject: [doc] Move a citation back into the introduction

Alternatively, we could duplicate the citation text in both index files.
---
 doc/sphinx/index.html.rst   | 5 -----
 doc/sphinx/introduction.rst | 5 +++++
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index 96ddd27027..9d90857061 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -89,8 +89,3 @@ 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/introduction.rst b/doc/sphinx/introduction.rst
index 5bb7bf542c..b8d2f6b6dc 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -35,6 +35,11 @@ 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