Reintroduce leftover parts; update index files; small fixes.

19 files changed, 204 insertions, 36 deletions

diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index a6dc15da55..5d257c7370 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -1,4 +1,4 @@
-.. _implicitcoercions:
+.. _coercions:
 
 Implicit Coercions
 ====================
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 2958d866ac..12fd038fb6 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -365,6 +365,21 @@ it is an atomic universe (i.e. not an algebraic max() universe).
 Explicit Universes
 -------------------
 
+.. insertprodn universe_name univ_constraint
+
+.. prodn::
+   universe_name ::= @qualid
+   | Set
+   | Prop
+   univ_annot ::= @%{ {* @universe_level } %}
+   universe_level ::= Set
+   | Prop
+   | Type
+   | _
+   | @qualid
+   univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
+   univ_constraint ::= @universe_name {| < | = | <= } @universe_name
+
 The syntax has been extended to allow users to explicitly bind names
 to universes and explicitly instantiate polymorphic definitions.
 
@@ -403,6 +418,37 @@ to universes and explicitly instantiate polymorphic definitions.
    .. exn:: Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead
       :undocumented:
 
+.. _printing-universes:
+
+Printing universes
+------------------
+
+.. flag:: Printing Universes
+
+   Turn this flag on to activate the display of the actual level of each
+   occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard flag, in
+   combination with :flag:`Printing All` can help to diagnose failures to unify
+   terms apparently identical but internally different in the Calculus of Inductive
+   Constructions.
+
+.. cmd:: Print {? Sorted } Universes {? Subgraph ( {* @qualid } ) } {? @string }
+   :name: Print Universes
+
+   This command can be used to print the constraints on the internal level
+   of the occurrences of :math:`\Type` (see :ref:`Sorts`).
+
+   The :n:`Subgraph` clause limits the printed graph to the requested names (adjusting
+   constraints to preserve the implied transitive constraints between
+   kept universes).
+
+   The :n:`Sorted` clause makes each universe
+   equivalent to a numbered label reflecting its level (with a linear
+   ordering) in the universe hierarchy.
+
+   :n:`@string` is an optional output filename.
+   If :n:`@string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
+   language, and can be processed by Graphviz tools. The format is
+   unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
 
 Polymorphic definitions
 ~~~~~~~~~~~~~~~~~~~~~~~
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
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 90173d65bf..a21f7e545c 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -28,9 +28,8 @@ especially about its foundations, please refer to :cite:`Del00`.
 Syntax
 ------
 
-The syntax of the tactic language is given below. See Chapter
-:ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used
-in these grammar rules. Various already defined entries will be used in this
+The syntax of the tactic language is given below.
+Various already defined entries will be used in this
 chapter: entries :token:`num`, :token:`int`, :token:`ident`
 :token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic`
 represent respectively natural and integer numbers,
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 127e4c6dbe..b660961279 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2977,6 +2977,41 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 Performing computations
 ---------------------------
 
+.. insertprodn red_expr pattern_occ
+
+.. prodn::
+   red_expr ::= red
+   | hnf
+   | simpl {? @delta_flag } {? @ref_or_pattern_occ }
+   | cbv {? @strategy_flag }
+   | cbn {? @strategy_flag }
+   | lazy {? @strategy_flag }
+   | compute {? @delta_flag }
+   | vm_compute {? @ref_or_pattern_occ }
+   | native_compute {? @ref_or_pattern_occ }
+   | unfold {+, @unfold_occ }
+   | fold {+ @one_term }
+   | pattern {+, @pattern_occ }
+   | @ident
+   delta_flag ::= {? - } [ {+ @smart_qualid } ]
+   strategy_flag ::= {+ @red_flags }
+   | @delta_flag
+   red_flags ::= beta
+   | iota
+   | match
+   | fix
+   | cofix
+   | zeta
+   | delta {? @delta_flag }
+   ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums }
+   | @one_term {? at @occs_nums }
+   occs_nums ::= {+ {| @num | @ident } }
+   | - {| @num | @ident } {* @int_or_var }
+   int_or_var ::= @int
+   | @ident
+   unfold_occ ::= @smart_qualid {? at @occs_nums }
+   pattern_occ ::= @one_term {? at @occs_nums }
+
 This set of tactics implements different specialized usages of the
 tactic :tacn:`change`.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7191444bac..2ba41ba9e5 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -747,6 +747,34 @@ Controlling display
    after each tactic.  The information is used by the Prooftree tool in Proof
    General. (https://askra.de/software/prooftree)
 
+.. _printing_constructions_full:
+
+Printing constructions in full
+------------------------------
+
+.. flag:: Printing All
+
+   Coercions, implicit arguments, the type of pattern matching, but also
+   notations (see :ref:`syntax-extensions-and-notation-scopes`) can obfuscate the behavior of some
+   tactics (typically the tactics applying to occurrences of subterms are
+   sensitive to the implicit arguments). Turning this flag on
+   deactivates all high-level printing features such as coercions,
+   implicit arguments, returned type of pattern matching, notations and
+   various syntactic sugar for pattern matching or record projections.
+   Otherwise said, :flag:`Printing All` includes the effects of the flags
+   :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`,
+   :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate
+   the high-level printing features, use the command ``Unset Printing All``.
+
+   .. note:: In some cases, setting :flag:`Printing All` may display terms
+      that are so big they become very hard to read.  One technique to work around
+      this is use :cmd:`Undelimit Scope` and/or :cmd:`Close Scope` to turn off the
+      printing of notations bound to particular scope(s).  This can be useful when
+      notations in a given scope are getting in the way of understanding
+      a goal, but turning off all notations with :flag:`Printing All` would make
+      the goal unreadable.
+
+      .. see a contrived example here: https://github.com/coq/coq/pull/11718#discussion_r415481854
 
 .. _vernac-controlling-the-reduction-strategies:
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index ea5ad79a80..e49073f593 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1383,10 +1383,29 @@ Abbreviations
    exception, if the right-hand side is just of the form :n:`@@qualid`,
    this conventionally stops the inheritance of implicit arguments.
 
+Numerals and strings
+--------------------
+
+.. insertprodn primitive_notations primitive_notations
+
+.. prodn::
+   primitive_notations ::= @numeral
+   | @string
+
+Numerals and strings have no predefined semantics in the calculus. They are
+merely notations that can be bound to objects through the notation mechanism.
+Initially, numerals are bound to Peano’s representation of natural
+numbers (see :ref:`datatypes`).
+
+.. note::
+
+   Negative integers are not at the same level as :n:`@num`, for this
+   would make precedence unnatural.
+
 .. _numeral-notations:
 
 Numeral notations
------------------
+~~~~~~~~~~~~~~~~~
 
 .. cmd:: Numeral Notation @qualid @qualid__parse @qualid__print : @scope_name {? @numeral_modifier }
    :name: Numeral Notation
@@ -1504,7 +1523,7 @@ Numeral notations
      opaque constants.
 
 String notations
------------------
+~~~~~~~~~~~~~~~~
 
 .. cmd:: String Notation @qualid @qualid__parse @qualid__print : @scope_name
    :name: String Notation