aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
diff options
context:
space:
mode:
authorThéo Zimmermann2020-11-13 10:08:48 +0100
committerThéo Zimmermann2020-11-14 13:40:45 +0100
commit15183aafe292695c54ae234a1210c08c8e3cd378 (patch)
treeda891e1212ee8a3d4ac4afac694bc9213632474a /doc/tools
parent51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff)
Move destructuring let syntax closer to its documentation.
Diffstat (limited to 'doc/tools')
-rw-r--r--doc/tools/docgram/common.edit_mlg5
-rw-r--r--doc/tools/docgram/orderedGrammar4
2 files changed, 8 insertions, 1 deletions
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