diff options
| author | Théo Zimmermann | 2018-09-25 12:46:08 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-25 12:46:08 +0200 |
| commit | edd0ede5ac057f6a7296351f608f162cd8b0a32b (patch) | |
| tree | 01e484be2f314ba39367440f07a1d7f52b3b0311 | |
| parent | 621d1071edd2f243d70c21c1a8f1706325a172eb (diff) | |
Fix title of Introduction chapter in HTML version.
And location of footnote.
| -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 |