Merge PR #13369: Move destructuring let syntax closer to its documentation.

Reviewed-by: jfehrle

4 files changed, 27 insertions, 10 deletions

diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 4ea3ea5e6d..79489c85f6 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -13,15 +13,18 @@ Let-in definitions
 .. prodn::
    term_let ::= let @name {? : @type } := @term in @term
    | let @name {+ @binder } {? : @type } := @term in @term
-   | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term
-   | let ' @pattern := @term {? return @term100 } in @term
-   | let ' @pattern in @pattern := @term return @term100 in @term
-
-:n:`let @ident := @term in @term’`
-denotes the local binding of :n:`@term` to the variable
-:n:`@ident` in :n:`@term`’. There is a syntactic sugar for let-in
-definition of functions: :n:`let @ident {+ @binder} := @term in @term’`
-stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
+   | @destructuring_let
+
+:n:`let @ident := @term__1 in @term__2` represents the local binding of
+the variable :n:`@ident` to the value :n:`@term__1` in :n:`@term__2`.
+
+:n:`let @ident {+ @binder} := @term__1 in @term__2` is an abbreviation
+for :n:`let @ident := fun {+ @binder} => @term__1 in @term__2`.
+
+.. seealso::
+
+   Extensions of the `let ... in ...` syntax are described in
+   :ref:`irrefutable-patterns`.
 
 .. index::
    single: ... : ... (type cast)
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 23389eba3b..8e62c2af13 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -86,6 +86,13 @@ Pattern-matching on terms inhabiting inductive type having only one
 constructor can be alternatively written using :g:`let … in …`
 constructions. There are two variants of them.
 
+.. insertprodn destructuring_let destructuring_let
+
+.. prodn::
+   destructuring_let ::= let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term
+   | let ' @pattern := @term {? return @term100 } in @term
+   | let ' @pattern in @pattern := @term return @term100 in @term
+
 
 First destructuring let syntax
 ++++++++++++++++++++++++++++++
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 4ad32e15eb..116fcaa87b 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -285,9 +285,12 @@ term_let: [
 (* Don't need to document that "( )" is equivalent to "()" *)
 | REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
 | WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200
+| MOVETO destructuring_let "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200
 | REPLACE "let" "'" pattern200 ":=" term200 "in" term200
-| WITH  "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
+| WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
 | DELETE "let" "'" pattern200 ":=" term200 case_type "in" term200
+| MOVETO destructuring_let "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
+| MOVETO destructuring_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
 ]
 
 atomic_constr: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index c697043f27..6b12d90d5d 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -473,6 +473,10 @@ ssr_dpat: [
 term_let: [
 | "let" name OPT ( ":" type ) ":=" term "in" term
 | "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term
+| destructuring_let
+]
+
+destructuring_let: [
 | "let" "(" LIST0 name SEP "," ")" OPT [ OPT [ "as" name ] "return" term100 ] ":=" term "in" term
 | "let" "'" pattern ":=" term OPT ( "return" term100 ) "in" term
 | "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term