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/sphinx/language') 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