From f2c59e19205eedc7d35f254b87a3acc457a8c36a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jun 2018 12:28:05 +0200
Subject: In "redundant clause" pattern-matching error, show also the pattern
 (#7777).

This is particularly useful when the pattern is part of a disjunction.

Maybe this could be improved though, not mentioning the pattern when
there is no disjunction, but that would be more work.
---
 test-suite/output/Cases.out | 2 ++
 test-suite/output/Cases.v   | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 419dcadb4c..dfab400baa 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -169,3 +169,5 @@ fun x : K => match x with
              | _ => 2
              end
      : K -> nat
+The command has indeed failed with message:
+Pattern "S _, _" is redundant in this clause.
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4740c009a4..e4fa7044e7 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -217,3 +217,6 @@ Check fun x => match x with a3 | a4 => 3 | _ => 2 end.
 Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end.
 Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end.
 Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end.
+
+(* Test redundant clause within a disjunctive pattern *)
+Fail Check fun n m => match n, m with 0, 0 | _, S _ | S 0, _ | S (S _ | _), _ => false end.
-- 
cgit v1.2.3