diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/index.html.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 5 |
2 files changed, 5 insertions, 5 deletions
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index 96ddd27027..9d90857061 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -89,8 +89,3 @@ 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/introduction.rst b/doc/sphinx/introduction.rst index 5bb7bf542c..b8d2f6b6dc 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -35,6 +35,11 @@ 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 |