From c571af2f95cccfbffe4e0b93525066676e7f652d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 27 Sep 2020 12:31:14 +0200
Subject: Reduce nitpick_ignore list a little.

---
 doc/sphinx/user-extensions/proof-schemes.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/user-extensions')

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index e05be7c2c2..8e23e61018 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -203,7 +203,7 @@ Generation of inversion principles with ``Derive`` ``Inversion``
    This command generates an inversion principle for the
    :tacn:`inversion ... using ...` tactic.  The first :token:`ident` is the name
    of the generated principle.  The second :token:`ident` should be an inductive
-   predicate, and :token:`binders` the variables occurring in the term
+   predicate, and :n:`{* @binder }` the variables occurring in the term
    :token:`term`. This command generates the inversion lemma for the sort
    :token:`sort` corresponding to the instance :n:`forall {* @binder }, @ident @term`.
    When applied, it is equivalent to having inverted the instance with the
-- 
cgit v1.2.3