diff options
| author | Clément Pit-Claudel | 2018-08-13 17:44:36 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | 81e55a33d518aa70cef62af3cdf3d6a013960ac6 (patch) | |
| tree | 64e83341c0a85f48eeb2c585128bda07848b85bc | |
| parent | 01e56b8ea3a0e3ba08e8f63d545c01be85b580b6 (diff) | |
[doc] Move a citation back into the introduction
Alternatively, we could duplicate the citation text in both index files.
| -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 |