diff options
| author | Hugo Herbelin | 2019-11-14 07:19:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:33:40 +0100 |
| commit | 50a39015ea0c86cdb6d368ff7f92ce2091085146 (patch) | |
| tree | 0b4f2fa58277a66f1c74bb757818179c29342f4f /interp/notation_ops.ml | |
| parent | d6467c2fea8a29634ca649850784c95ed5b9d4f4 (diff) | |
Fixing a notation printing bug (missing a @ to reflect absence of imp. args).
When a non-applied reference was matching a notation to the same
reference, implicit arguments were lost.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions