diff options
| -rw-r--r-- | doc/sphinx/index.html.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/index.latex.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 5 |
3 files changed, 12 insertions, 10 deletions
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index da129a3ed0..cf12b57414 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -1,11 +1,8 @@ -========================== - The Coq Reference Manual -========================== - .. _introduction: +========================== Introduction ------------- +========================== .. include:: introduction.rst @@ -89,3 +86,8 @@ License ------- .. include:: license.rst + +.. [#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/index.latex.rst b/doc/sphinx/index.latex.rst index 13bc1a19e7..af757f8746 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -7,6 +7,11 @@ Introduction .. include:: introduction.rst +.. [#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). + Credits ------- diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index b8d2f6b6dc..5bb7bf542c 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -35,11 +35,6 @@ are processed from a file. The `coqtop` read-eval-print-loop can also be used directly, for debugging purposes. - .. [#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). - - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact |