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 /test-suite | |
| 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 'test-suite')
| -rw-r--r-- | test-suite/output/Cases.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Cases.v | 3 |
2 files changed, 5 insertions, 0 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. |