diff options
| author | Hugo Herbelin | 2019-11-14 13:41:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:37:42 +0100 |
| commit | 9da7715108554a5105c012685e90b2fa563abf08 (patch) | |
| tree | d97038021444c19f43a7676044d9795c42cf2e69 /interp/constrintern.ml | |
| parent | 8d80875d230bd8af5611ec04bced1e5a17d058b0 (diff) | |
In printing patterns, distinguish the case of a notation to @id.
This is a case which conventionally deactivates implicit arguments.
Diffstat (limited to 'interp/constrintern.ml')
0 files changed, 0 insertions, 0 deletions