From 306a9dd33cc0f18e86f159c180ecd826f56f24db Mon Sep 17 00:00:00 2001 From: larsr Date: Thu, 12 Mar 2020 18:26:17 +0100 Subject: Update doc/sphinx/addendum/extended-pattern-matching.rst Co-Authored-By: Théo Zimmermann --- doc/sphinx/addendum/extended-pattern-matching.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3