diff options
| author | Vincent Laporte | 2019-02-14 06:47:54 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-14 07:04:42 +0000 |
| commit | 5446b141fb94fcbc5b05a0ef8ec362fd7485e91e (patch) | |
| tree | 4665ff837588666a5ded07356d9d683b93495cd9 | |
| parent | 398452805f1e3d0b2f4fac0d3a1b00ce9789e427 (diff) | |
[Manual] Fix a reference
| -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 d77690458d..3ec6c118af 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -295,7 +295,7 @@ By default, implicit arguments are omitted in patterns. So we write: end). But the possibility to use all the arguments is given by “``@``” implicit -explicitations (as for terms 2.7.11). +explicitations (as for terms, see :ref:`explicit-applications`). .. coqtop:: all |