diff options
| author | larsr | 2020-03-12 18:26:17 +0100 |
|---|---|---|
| committer | GitHub | 2020-03-12 18:26:17 +0100 |
| commit | 306a9dd33cc0f18e86f159c180ecd826f56f24db (patch) | |
| tree | 6cb97bf097ae82a0dfd94fb23f6e9906e024c103 | |
| parent | 3f2bfa50b1063bc981e3edfb8f5c6eaf53253643 (diff) | |
Update doc/sphinx/addendum/extended-pattern-matching.rst
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 989a83e802..8ec51e45ba 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -12,7 +12,7 @@ This section describes the full form of pattern matching in |Coq| terms. Patterns -------- -The full syntax of :g:`match` is presented in section :ref:`Syntax-of-terms`. +The full syntax of :g:`match` is presented in section :ref:`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 |