Add a good reference for Proof-General as suggested by Clément.

2 files changed, 16 insertions, 1 deletions

diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index bb881da04..bfa96621f 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -3,6 +3,21 @@
 @String{lnai  = "Lecture Notes in Artificial Intelligence"}
 @String{SV    = "{Sprin-ger-Verlag}"}
 
+@InCollection{Asp00,
+  Title        = {Proof General: A Generic Tool for Proof Development},
+  Author       = {Aspinall, David},
+  Booktitle    = {Tools and Algorithms for the Construction and
+               Analysis of Systems, {TACAS} 2000},
+  Publisher    = {Springer Berlin Heidelberg},
+  Year         = {2000},
+  Editor       = {Graf, Susanne and Schwartzbach, Michael},
+  Pages        = {38--43},
+  Series       = {Lecture Notes in Computer Science},
+  Volume       = {1785},
+  Doi          = {10.1007/3-540-46419-0_3},
+  ISBN         = {978-3-540-67282-1},
+}
+
 @Book{Bar81,
   author      = {H.P. Barendregt},
   publisher   = {North-Holland},
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 5a628f4ea..73da5e802 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 (available at https://proofgeneral.github.io/),
+   Emacs with Proof-General :cite:`Asp00` (available at https://proofgeneral.github.io/),
    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.