Reduce nitpick_ignore list a little.

4 files changed, 4 insertions, 7 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 11162ec96b..d533470f22 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -298,7 +298,7 @@ Summary of the commands
 .. cmd:: Class @inductive_definition {* with @inductive_definition }
 
    The :cmd:`Class` command is used to declare a typeclass with parameters
-   :token:`binders` and fields the declared record fields.
+   :n:`{* @binder }` and fields the declared record fields.
 
    Like any command declaring a record, this command supports the
    :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
@@ -337,7 +337,7 @@ Summary of the commands
    fields defined by :token:`field_def`, where each field must be a declared field of
    the class.
 
-   An arbitrary context of :token:`binders` can be put after the name of the
+   An arbitrary context of :n:`{* @binder }` can be put after the name of the
    instance and before the colon to declare a parameterized instance. An
    optional priority can be declared, 0 being the highest priority as for
    :tacn:`auto` hints. If the priority :token:`natural` is not specified, it defaults to the number
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index ee8784fc02..a8a574c861 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,11 +183,8 @@ todo_include_todos = False
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
-    'binders',
     'collection',
-    'modpath',
     'tactic',
-    'destruction_arg',
     'bindings',
     'induction_clause',
     'conversion',
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index ca69072cb9..f8375e93ce 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -217,7 +217,7 @@ usual implicit arguments disambiguation syntax.
 
 The syntax is also supported in internal binders. For instance, in the
 following kinds of expressions, the type of each declaration present
-in :token:`binders` can be bracketed to mark the declaration as
+in :n:`{* @binder }` can be bracketed to mark the declaration as
 implicit:
 * :n:`fun (@ident:forall {* @binder }, @type) => @term`,
 * :n:`forall (@ident:forall {* @binder }, @type), @type`,
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