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.
---
 vernac/himsg.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'vernac')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index c49ffe2679..0a316271e8 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1233,12 +1233,7 @@ let explain_wrong_numarg_inductive env ind n =
   str " expects " ++ decline_string n "argument" ++ str "."
 
 let explain_unused_clause env pats =
-(* Without localisation
-  let s = if List.length pats > 1 then "s" else "" in
-  (str ("Unused clause with pattern"^s) ++ spc () ++
-    hov 0 (pr_sequence pr_cases_pattern pats) ++ str ")")
-*)
-  str "This clause is redundant."
+  str "Pattern \"" ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) ++ strbrk "\" is redundant in this clause."
 
 let explain_non_exhaustive env pats =
   str "Non exhaustive pattern-matching: no clause found for " ++
-- 
cgit v1.2.3