Merge PR #12481: Minor improvements to the sections on basics and sorts.

Reviewed-by: jfehrle

4 files changed, 32 insertions, 30 deletions

diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 12fd038fb6..b0ef792bd1 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -361,6 +361,7 @@ it is an atomic universe (i.e. not an algebraic max() universe).
    to the sort :g:`Set` and only collapses floating universes between
    themselves.
 
+.. _explicit-universes:
 
 Explicit Universes
 -------------------
@@ -387,7 +388,7 @@ to universes and explicitly instantiate polymorphic definitions.
          Polymorphic Universe @ident
 
    In the monorphic case, this command declares a new global universe
-   named :g:`ident`, which can be referred to using its qualified name
+   named :token:`ident`, which can be referred to using its qualified name
    as well. Global universe names live in a separate namespace. The
    command supports the :attr:`universes(polymorphic)` attribute (or
    the ``Polymorphic`` prefix) only in sections, meaning the universe
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 9943e0aa76..955f48b772 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -44,10 +44,11 @@ fun and forall gets identical. Moreover, parentheses can be omitted in
 the case of a single sequence of bindings sharing the same type (e.g.:
 :g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`).
 
-.. index:: fun ... => ...
+.. index:: fun
+.. index:: forall
 
-Abstractions: fun
------------------
+Functions (fun) and function types (forall)
+-------------------------------------------
 
 .. insertprodn term_forall_or_fun term_forall_or_fun
 
@@ -69,11 +70,6 @@ a let-binder occurs in
 the list of binders, it is expanded to a let-in definition (see
 Section :ref:`let-in`).
 
-.. index:: forall
-
-Products: forall
-----------------
-
 The expression :n:`forall @ident : @type, @term` denotes the
 *product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`.
 As for abstractions, :g:`forall` is followed by a binder list, and products
@@ -92,8 +88,8 @@ Non dependent product types have a special notation: :g:`A -> B` stands for
 :g:`forall _ : A, B`. The *non dependent product* is used both to denote
 the propositional implication and function types.
 
-Applications
-------------
+Function application
+--------------------
 
 .. insertprodn term_application arg
 
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index d7f7259ab0..64b29c1c0b 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -417,8 +417,16 @@ more precise description of the scope of these settings):
 
 .. FIXME Convert "Extraction Language" to an option.
 
-Flags, options and tables are identified by a series of identifiers, each with an initial
-capital letter.
+.. insertprodn setting_name setting_name
+
+.. prodn::
+   setting_name ::= {+ @ident }
+
+..
+
+   Flags, options and tables are identified by a series of
+   identifiers.  By convention, each of the identifiers start with an
+   initial capital letter.
 
 Flags, options and tables appear in the HTML documentation in blue or
 gray boxes after the labels "Flag", "Option" and "Table".  In the pdf,
@@ -428,11 +436,6 @@ they appear after a boldface label.  They are listed in the
 .. cmd:: Set @setting_name {? {| @int | @string } }
    :name: Set
 
-   .. insertprodn setting_name setting_name
-
-   .. prodn::
-      setting_name ::= {+ @ident }
-
    If :n:`@setting_name` is a flag, no value may be provided; the flag
    is set to on.
    If :n:`@setting_name` is an option, a value of the appropriate type
@@ -533,4 +536,4 @@ Newly opened modules and sections inherit the current settings.
    :cmd:`Unset` commands.  If your goal is to define
    project-wide settings, you should rather use the command-line
    arguments ``-set`` and ``-unset`` for setting flags and options
-   (cf. :ref:`command-line-options`).
+   (see :ref:`command-line-options`).
diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst
index 03581b95dd..3517d70005 100644
--- a/doc/sphinx/language/core/sorts.rst
+++ b/doc/sphinx/language/core/sorts.rst
@@ -30,14 +30,16 @@ and :math:`\Set`.
 
 The sort :math:`\Prop` intends to be the type of logical propositions. If :math:`M` is a
 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.
+proofs of :math:`M`. An object :math:`m` belonging to :math:`M`
+:term:`witnesses <witness>` the fact that :math:`M` is
+provable. An object of type :math:`\Prop` is called a :gdef:`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
-equal). Objects of type :math:`\SProp` are called strict propositions.
+equal). Objects of type :math:`\SProp` are called
+:gdef:`strict propositions <strict proposition>`.
 See :ref:`sprop` for information about using
 :math:`\SProp`, and :cite:`Gilbert:POPL2019` for meta theoretical
 considerations.
@@ -66,12 +68,12 @@ Formally, we call :math:`\Sort` the set of sorts which is defined by:
 
    \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\}
 
-Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and
-:math:`\Type(i):\Type(i+1)`, are defined in Section :ref:`subtyping-rules`.
+Their properties, such as :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and
+:math:`\Type(i):\Type(i+1)`, are described in :ref:`subtyping-rules`.
 
 The user does not have to mention explicitly the index :math:`i` when
-referring to the universe :math:`\Type(i)`. One only writes :math:`\Type`. The system
-itself generates for each instance of :math:`\Type` a new index for the
+referring to the universe :math:`\Type(i)`. One only writes `Type`. The system
+itself generates for each instance of `Type` a new index for the
 universe and checks that the constraints between these indexes can be
 solved. From the user point of view we consequently have :math:`\Type:\Type`. We
 shall make precise in the typing rules the constraints between the
@@ -81,8 +83,8 @@ indices.
 .. _Implementation-issues:
 
 **Implementation issues** In practice, the Type hierarchy is
-implemented using *algebraic
-universes*. An algebraic universe :math:`u` is either a variable (a qualified
+implemented using algebraic universes.
+An :gdef:`algebraic universe` :math:`u` is either a variable (a qualified
 identifier with a number) or a successor of an algebraic universe (an
 expression :math:`u+1`), or an upper bound of algebraic universes (an
 expression :math:`\max(u_1 ,...,u_n )`), or the base universe (the expression
@@ -94,6 +96,6 @@ constraints between the universe variables is maintained globally. To
 ensure the existence of a mapping of the universes to the positive
 integers, the graph of constraints must remain acyclic. Typing
 expressions that violate the acyclicity of the graph of constraints
-results in a Universe inconsistency error.
+results in a :exn:`Universe inconsistency` error.
 
-.. seealso:: :ref:`printing-universes`.
+.. seealso:: :ref:`printing-universes`, :ref:`explicit-universes`.