Reintroduce leftover parts; update index files; small fixes.

5 files changed, 15 insertions, 6 deletions

diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 34a48b368b..85481043b2 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -109,7 +109,7 @@ Setting properties of a function's arguments
          clears argument scopes of :n:`@smart_qualid`
       `extra scopes`
          defines extra argument scopes, to be used in case of coercion to ``Funclass``
-         (see the :ref:`implicitcoercions` chapter) or with a computed type.
+         (see :ref:`coercions`) or with a computed type.
       `simpl nomatch`
          prevents performing a simplification step for :n:`@smart_qualid`
          that would expose a match construct in the head position.  See :ref:`Args_effect_on_unfolding`.
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index ca70890f4c..d97c98da9c 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -142,7 +142,7 @@ We build an infix notation == for a comparison predicate. Such
 notation will be overloaded, and its meaning will depend on the types
 of the terms that are compared.
 
-.. coqtop:: all
+.. coqtop:: all reset
 
   Module EQ.
     Record class (T : Type) := Class { cmp : T -> T -> Prop }.
diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
index 979a0a62e6..8dc5b99c4d 100644
--- a/doc/sphinx/language/extensions/evars.rst
+++ b/doc/sphinx/language/extensions/evars.rst
@@ -62,6 +62,15 @@ the syntax :n:`?[@ident]`. This is useful when the existential
 variable needs to be explicitly handled later in the script (e.g.
 with a named-goal selector, see :ref:`goal-selectors`).
 
+.. index:: _
+
+Inferable subterms
+------------------
+
+Expressions often contain redundant pieces of information. Subterms that can be
+automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will
+guess the missing piece of information.
+
 .. _explicit-display-existentials:
 
 Explicit displaying of existential instances for pretty-printing
diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst
index fc2ce03093..ed207ca743 100644
--- a/doc/sphinx/language/extensions/index.rst
+++ b/doc/sphinx/language/extensions/index.rst
@@ -16,13 +16,13 @@ language presented in the :ref:`previous chapter <core-language>`.
 .. toctree::
    :maxdepth: 1
 
-   ../gallina-extensions
+   evars
    implicit-arguments
-   ../../addendum/extended-pattern-matching
+   match
    ../../user-extensions/syntax-extensions
    arguments-command
    ../../addendum/implicit-coercions
    ../../addendum/type-classes
-   ../../addendum/canonical-structures
+   canonical
    ../../addendum/program
    ../../proof-engine/vernacular-commands
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 2aeace3cef..c5452d4590 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -287,7 +287,7 @@ This example emphasizes what the printing settings offer.
 Patterns
 --------
 
-The full syntax of :g:`match` is presented in section :ref:`term`.
+The full syntax of `match` is presented in :ref:`match`.
 Identifiers in patterns are either constructor names or variables. Any
 identifier that is not the constructor of an inductive or co-inductive
 type is considered to be a variable. A variable name cannot occur more