Fix note on implicit arguments in doc of functional induction.

1 files changed, 3 insertions, 3 deletions

diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index 40f9eedcf0..3625eac4a5 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -190,9 +190,9 @@ Tactics
 
    .. note::
       :n:`(@qualid {+ @term})` must be a correct full application
-         of :n:`@qualid`. In particular, the rules for implicit arguments are the
-         same as usual. For example use :n:`@qualid` if you want to write implicit
-         arguments explicitly.
+      of :n:`@qualid`. In particular, the rules for implicit arguments are the
+      same as usual. For example use :n:`@@qualid` if you want to write implicit
+      arguments explicitly.
 
    .. note::
       Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped.