diff options
| author | Clément Pit-Claudel | 2018-08-13 18:27:20 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | 7eced434fb9ceafc2d6e248aa5e49bbd6cd2e1fa (patch) | |
| tree | de3e2db007c9abb2a8b86903a1bb4dbdd611460a /doc/sphinx/index.latex.rst | |
| parent | dc4fc036cd361fe0d2943039e75570cf08a90868 (diff) | |
[doc] Create a separate zebibliography file for the LaTeX build
`.. bibliography::` puts the bibliography on its own page with its own title in
LaTeX, but includes it inline without a title in HTML [1], so we need to
maintain two separate copies of zebibliography.rst
[1] https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends
Diffstat (limited to 'doc/sphinx/index.latex.rst')
| -rw-r--r-- | doc/sphinx/index.latex.rst | 81 |
1 files changed, 81 insertions, 0 deletions
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst new file mode 100644 index 0000000000..13bc1a19e7 --- /dev/null +++ b/doc/sphinx/index.latex.rst @@ -0,0 +1,81 @@ +========================== + The Coq Reference Manual +========================== + +Introduction +------------ + +.. include:: introduction.rst + +Credits +------- + +.. include:: credits.rst + +License +------- + +.. include:: license.rst + +The language +------------ + +.. toctree:: + + language/gallina-specification-language + language/gallina-extensions + language/coq-library + language/cic + language/module-system + +The proof engine +---------------- + +.. toctree:: + + proof-engine/vernacular-commands + proof-engine/proof-handling + proof-engine/tactics + proof-engine/ltac + proof-engine/detailed-tactic-examples + proof-engine/ssreflect-proof-language + +User extensions +--------------- + +.. toctree:: + + user-extensions/syntax-extensions + user-extensions/proof-schemes + +Practical tools +--------------- + +.. toctree:: + + practical-tools/coq-commands + practical-tools/utilities + practical-tools/coqide + +Addendum +-------- + +.. toctree:: + + addendum/extended-pattern-matching + addendum/implicit-coercions + addendum/canonical-structures + addendum/type-classes + addendum/omega + addendum/micromega + addendum/extraction + addendum/program + addendum/ring + addendum/nsatz + addendum/generalized-rewriting + addendum/parallel-proof-processing + addendum/miscellaneous-extensions + addendum/universe-polymorphism + +.. toctree:: + zebibliography |