From 571834b2b43e4281ef4940ee5894d8191588bb6c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 29 Jul 2020 10:44:50 +0200
Subject: 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>
---
 test-suite/output/Cases.out |  3 +++
 test-suite/output/Cases.v   | 12 ++++++++++++
 2 files changed, 15 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3