diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-26 09:32:21 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-26 09:32:21 +0200 |
| commit | 7cc9bbd2c3f9faf4bbf66cae1bbd07289819161a (patch) | |
| tree | 62444b8be377ede63f5bc4c138138015b75a7227 /doc/sphinx/index.rst | |
| parent | a1fc621b943dbf904705dc88ed27c26daf4c5e72 (diff) | |
| parent | f8d1207b0d839274fb4358a0a7bd494f019cc681 (diff) | |
Merge PR #7851: Modernize the introduction of the reference manual.
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 f3ae49381..baf2e0d98 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -84,3 +84,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). |