diff options
| author | Hugo Herbelin | 2020-07-29 10:44:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-05 16:19:12 +0200 |
| commit | 571834b2b43e4281ef4940ee5894d8191588bb6c (patch) | |
| tree | 4efc006b604db1cf23657053271c366683e6e8dd /test-suite | |
| parent | 6d3a9220204de22e0b81dc961d2eb269128b5c2e (diff) | |
Wish #12762: warning on duplicated catch-all pattern with unused named variable.
An identifier starting with _ deactivates the warning.
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Cases.out | 3 | ||||
| -rw-r--r-- | test-suite/output/Cases.v | 12 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index da2fc90fc3..01564e7f25 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -178,3 +178,6 @@ match N with | _ => Node end : Tree -> Tree +File "stdin", line 253, characters 4-5: +Warning: Unused variable B catches more than one case. +[unused-pattern-matching-variable,pattern-matching] diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 262ec2b677..2d8a8b359c 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -242,3 +242,15 @@ end. Print stray. End Bug11231. + +Module Wish12762. + +Inductive foo := a | b | c. + +Definition bar (f : foo) := + match f with + | a => 0 + | B => 1 + end. + +End Wish12762. |