diff options
| author | Maxime Dénès | 2018-05-14 13:43:41 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-14 13:43:41 +0200 |
| commit | 9e3989f949c1e3f20031d9af5a7bc89d97f5a951 (patch) | |
| tree | a3bc0f6a7f80840f84109460a3169726ffffe590 /doc/sphinx/user-extensions | |
| parent | 4094a8c2cac668db112fc84f5d1b287eacbf6700 (diff) | |
| parent | 805d78d12443d9df646362c024bfa83466c27fdd (diff) | |
Merge PR #7374: [sphinx] More fatal warnings.
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 5 |
2 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index e12e4d897a..682553c31b 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -26,6 +26,7 @@ induction for objects in type `identᵢ`. natural in case of inductively defined relations. .. cmdv:: Scheme Equality for @ident + :name: Scheme Equality Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident` involves some other inductive types, their equality has to be defined first. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6958b5f265..3b95a37ed3 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -916,9 +916,8 @@ Binding arguments of a constant to an interpretation scope .. seealso:: - :cmd:`About @qualid` - The command to show the scopes bound to the arguments of a - function is described in Section 2. + The command :cmd:`About` can be used to show the scopes bound to the + arguments of a function. .. note:: |