From 6631e485b86747bac15a85cd83e0c62d824ce8ce Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 20 Jun 2018 16:16:28 +0200 Subject: Add a good reference for Proof-General as suggested by Clément. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- doc/sphinx/introduction.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx/introduction.rst') 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. -- cgit v1.2.3