Mention Company-Coq as well.

We put it in a footnote otherwise the sentence was starting to be really long.
Footnotes need to be in index.rst to really appear at the bottom of the index page.

3 files changed, 15 insertions, 1 deletions

diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index bfa96621f..3574bf675 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -305,6 +305,15 @@ the Calculus of Inductive Constructions}},
   year        = {1995}
 }
 
+@InProceedings{Pit16,
+  Title        = {Company-Coq: Taking Proof General one step closer to a real IDE},
+  Author       = {Pit-Claudel, Clément and Courtieu, Pierre},
+  Booktitle    = {CoqPL'16: The Second International Workshop on Coq for PL},
+  Year         = {2016},
+  Month        = jan,
+  Doi          = {10.5281/zenodo.44331},
+}
+
 @Book{RC95,
   author      = {di~Cosmo, R.},
   title       = {Isomorphisms of Types: from $\lambda$-calculus to information
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 136f9088b..7baa4c450 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -81,3 +81,8 @@ This material (the Coq Reference Manual) may be distributed only subject to the
 terms and conditions set forth in the Open Publication License, v1.0 or later
 (the latest version is presently available at
 http://www.opencontent.org/openpub). Options A and B are not elected.
+
+.. [#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 73da5e802..49f5db342 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -34,7 +34,7 @@ are processed from a file.
    step, and query the system for available theorems and definitions. The
    interactive mode is generally run with the help of an IDE, such
    as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`,
-   Emacs with Proof-General :cite:`Asp00` (available at https://proofgeneral.github.io/),
+   Emacs with Proof-General :cite:`Asp00` [#PG]_,
    or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq).
    The `coqtop` read-eval-print-loop can also be used directly, for debugging
    purposes.