Reintroduce leftover parts; update index files; small fixes.

13 files changed, 71 insertions, 30 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 5f74958712..768c83150e 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -519,16 +519,6 @@ One can consequently derive the following property.
    \WF{E;E′}{Γ}
 
 
-.. _Co-inductive-types:
-
-Co-inductive types
-----------------------
-
-The implementation contains also co-inductive definitions, which are
-types inhabited by infinite objects. More information on co-inductive
-definitions can be found in :cite:`Gimenez95b,Gim98,GimCas05`.
-
-
 .. _The-Calculus-of-Inductive-Construction-with-impredicative-Set:
 
 The Calculus of Inductive Constructions with impredicative Set
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index 51860aec0d..c034b7f302 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -14,6 +14,9 @@ constructors. Infinite objects are introduced by a non-ending (but
 effective) process of construction, defined in terms of the constructors
 of the type.
 
+More information on co-inductive definitions can be found in
+:cite:`Gimenez95b,Gim98,GimCas05`.
+
 .. cmd:: CoInductive @inductive_definition {* with @inductive_definition }
 
    This command introduces a co-inductive type.
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 679022a5b1..0e637e5aa3 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -72,11 +72,12 @@ Section :ref:`typing-rules`.
 .. cmd:: {| Definition | Example } @ident_decl @def_body
    :name: Definition; Example
 
-   .. insertprodn def_body def_body
+   .. insertprodn def_body reduce
 
    .. prodn::
       def_body ::= {* @binder } {? : @type } := {? @reduce } @term
       | {* @binder } : @type
+      reduce ::= Eval @red_expr in
 
    These commands bind :n:`@term` to the name :n:`@ident` in the environment,
    provided that :n:`@term` is well-typed.  They can take the :attr:`local` :term:`attribute`,
diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst
index 5e83672463..de780db267 100644
--- a/doc/sphinx/language/core/index.rst
+++ b/doc/sphinx/language/core/index.rst
@@ -34,10 +34,17 @@ will have to check their output.
    :maxdepth: 1
 
    basic
-   ../gallina-specification-language
+   sorts
+   assumptions
+   definitions
+   conversion
    ../cic
+   variants
    records
+   inductive
+   coinductive
+   sections
+   modules
+   primitive
    ../../addendum/universe-polymorphism
    ../../addendum/sprop
-   sections
-   ../module-system
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 189e1008e8..53c8cd4701 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -333,10 +333,6 @@ Mutually defined inductive types
    A generic command :cmd:`Scheme` is useful to build automatically various
    mutual induction principles.
 
-.. [1]
-   Except if the inductive type is empty in which case there is no
-   equation that can be used to infer the return type.
-
 .. index::
    single: fix
 
@@ -548,7 +544,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort`
 
    which corresponds to the result of the |Coq| declaration:
 
-   .. coqtop:: in
+   .. coqtop:: in reset
 
       Inductive list (A:Set) : Set :=
       | nil : list A
@@ -1103,7 +1099,7 @@ respect to the hierarchy :math:`\Prop ⊂ \Set_p ⊂ \Type` where :math:`\Set_p`
 (i.e. an inductive definition of which all inductive types are
 singleton – see Section :ref:`Destructors`) is set in :math:`\Prop`, a small non-singleton
 inductive type is set in :math:`\Set` (even in case :math:`\Set` is impredicative – see
-Section The-Calculus-of-Inductive-Construction-with-impredicative-Set_),
+:ref:`The-Calculus-of-Inductive-Construction-with-impredicative-Set`),
 and otherwise in the Type hierarchy.
 
 Note that the side-condition about allowed elimination sorts in the rule
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 74977e7088..b06dd2f1ab 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -864,7 +864,7 @@ The theories developed in |Coq| are stored in *library files* which are
 hierarchically classified into *libraries* and *sublibraries*. To
 express this hierarchy, library names are represented by qualified
 identifiers qualid, i.e. as list of identifiers separated by dots (see
-:ref:`gallina-identifiers`). For instance, the library file ``Mult`` of the standard
+:ref:`qualified-names`). For instance, the library file ``Mult`` of the standard
 |Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts
 the name of a library is called a *library root*. All library files of
 the standard library of |Coq| have the reserved root |Coq| but library
@@ -875,8 +875,14 @@ started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-opt
 
 .. _qualified-names:
 
-Qualified names
-~~~~~~~~~~~~~~~
+Qualified identifiers
+---------------------
+
+.. insertprodn qualid field_ident
+
+.. prodn::
+   qualid ::= @ident {* @field_ident }
+   field_ident ::= .@ident
 
 Library files are modules which possibly contain submodules which
 eventually contain constructions (axioms, parameters, definitions,
diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst
index 3fa5f826df..8307a02d6d 100644
--- a/doc/sphinx/language/core/sorts.rst
+++ b/doc/sphinx/language/core/sorts.rst
@@ -1,8 +1,27 @@
-.. _Sorts:
+.. index::
+   single: Set (sort)
+   single: SProp
+   single: Prop
+   single: Type
+
+.. _sorts:
 
 Sorts
 ~~~~~~~~~~~
 
+.. insertprodn sort universe_expr
+
+.. prodn::
+   sort ::= Set
+   | Prop
+   | SProp
+   | Type
+   | Type @%{ _ %}
+   | Type @%{ @universe %}
+   universe ::= max ( {+, @universe_expr } )
+   | @universe_expr
+   universe_expr ::= @universe_name {? + @num }
+
 The types of types are called :gdef:`sort`\s.
 
 All sorts have a type and there is an infinite well-founded typing
@@ -13,6 +32,8 @@ The sort :math:`\Prop` intends to be the type of logical propositions. If :math:
 logical proposition then it denotes the class of terms representing
 proofs of :math:`M`. An object :math:`m` belonging to :math:`M` witnesses the fact that :math:`M` is
 provable. An object of type :math:`\Prop` is called a proposition.
+We denote propositions by :n:`@form`.
+This constitutes a semantic subclass of the syntactic class :n:`@term`.
 
 The sort :math:`\SProp` is like :math:`\Prop` but the propositions in
 :math:`\SProp` are known to have irrelevant proofs (all proofs are
@@ -24,6 +45,8 @@ considerations.
 The sort :math:`\Set` intends to be the type of small sets. This includes data
 types such as booleans and naturals, but also products, subsets, and
 function types over these data types.
+We denote specifications (program types) by :n:`@specif`.
+This constitutes a semantic subclass of the syntactic class :n:`@term`.
 
 :math:`\SProp`, :math:`\Prop` and :math:`\Set` themselves can be manipulated as ordinary terms.
 Consequently they also have a type. Because assuming simply that :math:`\Set`
diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index 315e97687b..6d4676b3c4 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -52,6 +52,8 @@ Private (matching) inductive types
 
 .. index:: match ... with ...
 
+.. _match:
+
 Definition by cases: match
 --------------------------
 
@@ -194,3 +196,7 @@ a type with annotations. For this third subcase, both the clauses ``as`` and
 There are specific notations for case analysis on types with one or two
 constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see
 Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`).
+
+.. [1]
+   Except if the inductive type is empty in which case there is no
+   equation that can be used to infer the return type.
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