diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 4 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 2 |
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 |