Merge PR #12768: Granting wish #12762: warning on duplicated catch-all pattern-matching clause with unused named variable

Reviewed-by: jfehrle
Reviewed-by: vbgl
Ack-by: gares

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.