diff options
| author | coqbot-app[bot] | 2020-11-14 21:45:11 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-14 21:45:11 +0000 |
| commit | 6b7d6be8eb0b8c12804a53475e33c1489e3bc61e (patch) | |
| tree | 40262a9fc8d62a2491d9e5c0f2e49d79751ebe3a /doc/tools/docgram/common.edit_mlg | |
| parent | 9a93f5836a5f7bab81384314ac11ff0aac7d1b7f (diff) | |
| parent | 15183aafe292695c54ae234a1210c08c8e3cd378 (diff) | |
Merge PR #13369: Move destructuring let syntax closer to its documentation.
Reviewed-by: jfehrle
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 5 |
1 files changed, 4 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: [ |