From e83a92d8855f1b2f99f2960454898985593d4cb6 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 16 May 2020 15:41:21 +0200
Subject: Fix note on implicit arguments in doc of functional induction.

---
 doc/sphinx/using/libraries/funind.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx/using')

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.
-- 
cgit v1.2.3