Merge PR #12085: Convert ltac2 chapter to use prodn, update syntax

Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
Ack-by: ppedrot

1 files changed, 4 insertions, 0 deletions

diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index d6a828521f..34752a4c4d 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -90,6 +90,10 @@ 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