From f8d1207b0d839274fb4358a0a7bd494f019cc681 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 20 Jun 2018 16:59:09 +0200 Subject: 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. --- doc/sphinx/biblio.bib | 9 +++++++++ doc/sphinx/index.rst | 5 +++++ doc/sphinx/introduction.rst | 2 +- 3 files changed, 15 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') 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. -- cgit v1.2.3