From bc4f73821733365fb5882f455ca503feaa96f11f Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 16 May 2019 16:47:35 -0400 Subject: [refman] Give explicit names to the various 'Arguments' commands --- doc/sphinx/user-extensions/syntax-extensions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/sphinx/user-extensions') 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 `). Whether the argument of a function has some type ``type`` is determined statically. For instance, if ``f`` is a polymorphic function of type -- cgit v1.2.3