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..0f2f7b4897
--- /dev/null
+++ b/doc/sphinx/index.latex.rst
@@ -0,0 +1,81 @@
+==========================
+ The Coq Reference Manual
+==========================
+
+Introduction
+------------
+
+.. include:: introduction.rst
+
+Credits
+-------
+
+.. include:: credits-wrapper.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