diff options
| author | Hugo Herbelin | 2018-06-12 12:28:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-07-25 18:41:48 +0200 |
| commit | f2c59e19205eedc7d35f254b87a3acc457a8c36a (patch) | |
| tree | c209bb94c4269d716975abe54981488b47fd2387 /vernac | |
| parent | 523de4f878293cf1d582bd70300b34d497e705b3 (diff) | |
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.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 7 |
1 files changed, 1 insertions, 6 deletions
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 " ++ |