diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-20 16:16:28 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-20 16:59:58 +0200 |
| commit | 6631e485b86747bac15a85cd83e0c62d824ce8ce (patch) | |
| tree | 5a0c8f214bf5951be52b3ffd3bd2b78135055a4d /doc/sphinx/introduction.rst | |
| parent | a321962205a26fac6ec16929636ea748e572905e (diff) | |
Add a good reference for Proof-General as suggested by Clément.
Diffstat (limited to 'doc/sphinx/introduction.rst')
| -rw-r--r-- | doc/sphinx/introduction.rst | 2 |
1 files changed, 1 insertions, 1 deletions
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. |