diff options
Diffstat (limited to 'doc/sphinx/language/extensions/match.rst')
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 028d0aaf57..b4558ef07f 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -289,7 +289,7 @@ This example emphasizes what the printing settings offer. Patterns -------- -The full syntax of `match` is presented in :ref:`match`. +The full syntax of `match` is presented in :ref:`match_term`. Identifiers in patterns are either constructor names or variables. Any identifier that is not the constructor of an inductive or co-inductive type is considered to be a variable. A variable name cannot occur more |