aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
authorHugo Herbelin2019-11-14 08:26:14 +0100
committerHugo Herbelin2020-02-22 22:37:15 +0100
commit14196d8ab425f67faf3995bd29a003de3b2e87ac (patch)
tree37379c35029ee6269a9796f42f360e329b4f9a23 /plugins/syntax
parent556e9dde62b6822db20bd5c7e6e6a67bc717c408 (diff)
Propagate implicit arguments in all notations for partial applications.
This was done for abbreviations but not string notations. This adopts the policy proposed in #11091 to make parsing and printing consistent.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions