diff options
| author | Clément Pit-Claudel | 2019-05-16 16:47:35 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-05-22 14:35:47 -0400 |
| commit | bc4f73821733365fb5882f455ca503feaa96f11f (patch) | |
| tree | b4b101642613cd8130584376cafd04faee6643b7 /doc/sphinx/user-extensions | |
| parent | 5c5bd952e9c28c3acf740fcdced03b2b7145076d (diff) | |
[refman] Give explicit names to the various 'Arguments' commands
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6da42f4a48..6a681d83f0 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1143,8 +1143,8 @@ Binding types of arguments to an interpretation scope scope of operations on the natural numbers), it may be convenient to bind it to this type. When a scope ``scope`` is bound to a type ``type``, any new function defined later on gets its arguments of type ``type`` interpreted by default in - scope scope (this default behavior can however be overwritten by explicitly - using the command :cmd:`Arguments`). + scope ``scope`` (this default behavior can however be overwritten by explicitly + using the command :cmd:`Arguments <Arguments (scopes)>`). Whether the argument of a function has some type ``type`` is determined statically. For instance, if ``f`` is a polymorphic function of type |