diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 37 |
2 files changed, 44 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst b/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst new file mode 100644 index 0000000000..c9e941743c --- /dev/null +++ b/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst @@ -0,0 +1,7 @@ +- **Added:** + Warning on unused variables in pattern-matching branches of + :n:`match` serving as catch-all branches for at least two distinct + patterns. + (`#12768 <https://github.com/coq/coq/pull/12768>`_, + fixes `#12762 <https://github.com/coq/coq/issues/12762>`_, + by Hugo Herbelin). diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 561262262b..3c1983ee97 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -290,6 +290,43 @@ This example emphasizes what the printing settings offer. Print snd. +Conventions about unused pattern-matching variables +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Pattern-matching variables that are not used on the right-hand side of ``=>`` are +considered the sign of a potential error. For instance, it could +result from an undetected mispelled constant constructor. By default, +a warning is issued in such situations. + +.. warn:: Unused variable @ident catches more than one case. + + This indicates that an unused pattern variable :token:`ident` + occurs in a pattern-matching clause used to complete at least two + cases of the pattern-matching problem. + + The warning can be deactivated by using a variable name starting + with ``_`` or by setting ``Set Warnings + "-unused-pattern-matching-variable"``. + + Here is an example where the warning is activated. + + .. example:: + + .. coqtop:: none + + Set Warnings "-unused-pattern-matching-variable". + + .. coqtop:: all + + Definition is_zero (o : option nat) := match o with + | Some 0 => true + | x => false + end. + + .. coqtop:: none + + Set Warnings "+unused-pattern-matching-variable". + Patterns -------- |