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 /test-suite | |
| 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 'test-suite')
| -rw-r--r-- | test-suite/output/Notations.out | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 2966c1126d..53ad8a9612 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -107,8 +107,8 @@ fun x : option Z => match x with end : option Z -> Z fun x : option Z => match x with - | SOME2 x0 => x0 - | NONE2 => 0 + | SOME3 _ x0 => x0 + | NONE3 _ => 0 end : option Z -> Z fun x : list ?T => |