diff options
| author | Hugo Herbelin | 2019-11-14 08:26:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:37:15 +0100 |
| commit | 14196d8ab425f67faf3995bd29a003de3b2e87ac (patch) | |
| tree | 37379c35029ee6269a9796f42f360e329b4f9a23 /plugins/syntax | |
| parent | 556e9dde62b6822db20bd5c7e6e6a67bc717c408 (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
