aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum/extended-pattern-matching.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/addendum/extended-pattern-matching.rst')
-rw-r--r--doc/sphinx/addendum/extended-pattern-matching.rst3
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index 64d4eddf04..1d3b661732 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -305,6 +305,8 @@ explicitations (as for terms 2.7.11).
end).
+.. _matching-dependent:
+
Matching objects of dependent types
-----------------------------------
@@ -414,6 +416,7 @@ length, by writing
I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`.
+.. _match-in-patterns:
Patterns in ``in``
~~~~~~~~~~~~~~~~~~