Merge PR #9542: [Manual] Don’t use `Undo`; and other cleaning

Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes

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