diff options
| author | Hugo Herbelin | 2019-11-13 13:17:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:33:40 +0100 |
| commit | d6467c2fea8a29634ca649850784c95ed5b9d4f4 (patch) | |
| tree | 39e7d10a482a3eff2ec139e3115dd0ca7d7713a5 /interp/notation_ops.ml | |
| parent | fe86fb5561f2bbde86236d8c91e973df4393049f (diff) | |
Fixing anomaly from #11091 (incompatible printing with notation and imp. args).
We fix also an index error in deciding when to explicit print a
non-inferable implicit argument.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions