diff options
| author | Hugo Herbelin | 2019-11-14 07:31:37 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:34:37 +0100 |
| commit | 556e9dde62b6822db20bd5c7e6e6a67bc717c408 (patch) | |
| tree | 65d0d09683a896d4aecba98139e45edd608a19a7 /interp/constrintern.ml | |
| parent | 67e16fdeef26455d0afa357e31de8f7b3f772034 (diff) | |
Deactivate implicit arguments in printing notations bound to "@f".
This is to match the parsing policy (see #11091).
In particular, we deactivate also argument scopes, consistently with
what is done at parsing time.
Diffstat (limited to 'interp/constrintern.ml')
0 files changed, 0 insertions, 0 deletions