diff options
| author | larsr | 2020-03-12 17:20:18 +0100 |
|---|---|---|
| committer | GitHub | 2020-03-12 17:20:18 +0100 |
| commit | 3f2bfa50b1063bc981e3edfb8f5c6eaf53253643 (patch) | |
| tree | ae574fd4a357653a04130fb2d6703637f6a16dc1 | |
| parent | 1a7cdc1da9bff2e46acdd5c07a7eee5dcd27d731 (diff) | |
Fixed link to "match" syntax.
and removed the now incorrect "section 8.2.3" reference, as it is the same as the "refine" link.
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 15f42591ce..989a83e802 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -5,8 +5,6 @@ Extended pattern matching :Authors: Cristina Cornes and Hugo Herbelin -.. TODO links to figures - This section describes the full form of pattern matching in |Coq| terms. .. |rhs| replace:: right hand sides @@ -14,7 +12,7 @@ This section describes the full form of pattern matching in |Coq| terms. Patterns -------- -The full syntax of match is presented in Figures 1.1 and 1.2. +The full syntax of :g:`match` is presented in section :ref:`Syntax-of-terms`. 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 @@ -496,9 +494,8 @@ We can use multiple patterns to write the proof of the lemma In the example of :g:`dec`, the first match is dependent while the second is not. -The user can also use match in combination with the tactic :tacn:`refine` (see -Section 8.2.3) to build incomplete proofs beginning with a match -construction. +The user can also use match in combination with the tactic :tacn:`refine` +to build incomplete proofs beginning with a :g:`match` construction. Pattern-matching on inductive objects involving local definitions |