diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-29 00:38:54 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-09 10:35:10 +0200 |
| commit | 88c702dfac4adb8bf590a2bdf30e76c7c6cb892f (patch) | |
| tree | a619bc1c3dd2c11fa6ce409cc6ba8fbb0759a648 /doc/sphinx/user-extensions | |
| parent | 52e58d368bb0646cc05684995d6e00da370736e6 (diff) | |
[sphinx] Fix new warnings related to tacn, cmd, opt...
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 e12e4d897..682553c31 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 6958b5f26..3b95a37ed 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:: |