diff options
| author | Hugo Herbelin | 2020-11-06 04:57:46 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-06 05:06:09 +0100 |
| commit | c470b92b8d61fc52b1d7e8697efd36a75ddec9d1 (patch) | |
| tree | 76fb7d4fb407467557c1a2dc21233cf679097d16 /interp | |
| parent | d276a494d29ea69c6a60b16da5dddb9d39f287ca (diff) | |
The "( X in t )" hack used in the syntax of ssr rewrite may be only parsing.
This is the only notation to date which breaks the heuristics of
prefering the more precise notations for printing (see #12986).
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions