diff options
| author | Hugo Herbelin | 2019-11-14 13:42:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:37:42 +0100 |
| commit | a905e70df85ef7bf700bb3d6a1b48ae180dfa987 (patch) | |
| tree | f80547285ccfee9f0d64f6dabd9c0a6b72e1c181 /plugins/syntax/string_notation.mli | |
| parent | 9da7715108554a5105c012685e90b2fa563abf08 (diff) | |
Inherit arguments scopes in pattern notations bound to some @id.
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions