diff options
| author | Pierre-Marie Pédrot | 2018-07-26 11:06:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-26 11:06:23 +0200 |
| commit | b13c954c49f546ecbbc5f73d32e69348408e2ad4 (patch) | |
| tree | 95b3ba6a60246b511109951736e7f6bdb769e359 | |
| parent | 3f6383c4042390b05651d20f04d4405589ffd8f3 (diff) | |
| parent | f2c59e19205eedc7d35f254b87a3acc457a8c36a (diff) | |
Merge PR #7786: In "redundant clause" pattern-matching error, show also the pattern (closes #7777)
| -rw-r--r-- | test-suite/output/Cases.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Cases.v | 3 | ||||
| -rw-r--r-- | vernac/himsg.ml | 7 |
3 files changed, 6 insertions, 6 deletions
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. diff --git a/vernac/himsg.ml b/vernac/himsg.ml index e208d176bb..b9c47ff475 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1227,12 +1227,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 " ++ |