Merge PR #11601: [refman] Move chapters into new structure.

Reviewed-by: jfehrle

1 files changed, 26 insertions, 0 deletions

diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst
new file mode 100644
index 0000000000..f22927d627
--- /dev/null
+++ b/doc/sphinx/language/extensions/index.rst
@@ -0,0 +1,26 @@
+.. _extensions:
+
+===================
+Language extensions
+===================
+
+Elaboration extends the language accepted by the Coq kernel to make it
+easier to use.  For example, this lets the user omit most type
+annotations because they can be inferred, call functions with implicit
+arguments which will be inferred as well, extend the syntax with
+notations, factorize branches when pattern-matching, etc.  In this
+chapter, we present these language extensions and we give some
+explanations on how this language is translated down to the core
+language presented in the :ref:`previous chapter <core-language>`.
+
+.. toctree::
+   :maxdepth: 1
+
+   ../gallina-extensions
+   ../../addendum/extended-pattern-matching
+   ../../user-extensions/syntax-extensions
+   ../../addendum/implicit-coercions
+   ../../addendum/type-classes
+   ../../addendum/canonical-structures
+   ../../addendum/program
+   ../../proof-engine/vernacular-commands