Convert ltac2 chapter to use prodn, update syntax

3 files changed, 14 insertions, 3 deletions

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 64b29c1c0b..1f0d696d99 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -227,6 +227,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
         | @term_match
         | @term_record
         | @term_generalizing
+        | [| {*; @term } %| @term {? : @type } |] {? @univ_annot }
         | @term_ltac
         | ( @term )
         qualid_annotated ::= @qualid {? @univ_annot }
diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst
index 0f27b65107..6b031cfea3 100644
--- a/doc/sphinx/language/core/conversion.rst
+++ b/doc/sphinx/language/core/conversion.rst
@@ -5,8 +5,14 @@ Conversion rules
 
 In |Cic|, there is an internal reduction mechanism. In particular, it
 can decide if two programs are *intentionally* equal (one says
-*convertible*). Convertibility is described in this section.
+:term:`convertible`). Convertibility is described in this section.
 
+α-conversion
+~~~~~~~~~~~~
+
+Two terms are :gdef:`α-convertible <alpha-convertible>` if they are syntactically
+equal ignoring differences in the names of variables bound within the expression.
+For example `forall x, x + 0 = x` is α-convertible with `forall y, y + 0 = y`.
 
 .. _beta-reduction:
 
@@ -153,7 +159,7 @@ relation :math:`t` reduces to :math:`u` in the global environment
 reductions β, δ, ι or ζ.
 
 We say that two terms :math:`t_1` and :math:`t_2` are
-*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the
+*βδιζη-convertible*, or simply :gdef:`convertible`, or *equivalent*, in the
 global environment :math:`E` and local context :math:`Γ` iff there
 exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright
 … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index b4558ef07f..34752a4c4d 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -90,11 +90,15 @@ constructions. There are two variants of them.
 First destructuring let syntax
 ++++++++++++++++++++++++++++++
 
+.. todo explain that this applies to all of the "let" constructs (Gallina, Ltac1 and Ltac2)
+   also add "irrefutable pattern" to the glossary
+   note that in Ltac2 an upper case ident is a constructor, lower case is a variable
+
 The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1`
 performs case analysis on :n:`@term__0` whose type must be an
 inductive type with exactly one constructor.  The number of variables
 :n:`@ident__i` must correspond to the number of arguments of this
-contrustor.  Then, in :n:`@term__1`, these variables are bound to the
+constructor.  Then, in :n:`@term__1`, these variables are bound to the
 arguments of the constructor in :n:`@term__0`.  For instance, the
 definition