diff options
| author | Théo Zimmermann | 2020-09-27 12:31:14 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-09-27 12:31:14 +0200 |
| commit | c571af2f95cccfbffe4e0b93525066676e7f652d (patch) | |
| tree | 68d4f8fd36d03482d2a33ee5e64d5ff813ebbe2c /doc/sphinx/addendum | |
| parent | 9c2228ff011dc6188b70084fa1e1a5158affcf24 (diff) | |
Reduce nitpick_ignore list a little.
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 4 |
1 files changed, 2 insertions, 2 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 |