From ed8c756d58f24645a05c4cafcdc3e260f75e8b24 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 29 Jul 2020 10:59:40 +0200 Subject: Change log for #12768. Co-authored-by: Jim Fehrle --- ...12768-master+warn-non-underscore-catch-all-pattern-matching.rst | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst (limited to 'doc') 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 `_, + fixes `#12762 `_, + by Hugo Herbelin). -- cgit v1.2.3 From 3c73900038e904e007e0e83d53ac040dfc951fb0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 28 Sep 2020 20:33:29 +0200 Subject: Documenting warning about unused variables in pattern clauses. Co-authored-by: Jim Fehrle --- doc/sphinx/language/extensions/match.rst | 37 ++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index c36b9deef3..e6188b8023 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 -------- -- cgit v1.2.3