diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-20 16:59:09 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-20 16:59:58 +0200 |
| commit | f8d1207b0d839274fb4358a0a7bd494f019cc681 (patch) | |
| tree | 41535b70e42f9b61a8b88a660ac7d6cef0eb3fde /doc/sphinx/index.rst | |
| parent | 6631e485b86747bac15a85cd83e0c62d824ce8ce (diff) | |
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.
Diffstat (limited to 'doc/sphinx/index.rst')
| -rw-r--r-- | doc/sphinx/index.rst | 5 |
1 files changed, 5 insertions, 0 deletions
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). |