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/changes.rst | 4 ++-- doc/sphinx/language/gallina-extensions.rst | 3 +++ doc/sphinx/proof-engine/tactics.rst | 2 +- doc/sphinx/proof-engine/vernacular-commands.rst | 2 +- doc/sphinx/user-extensions/syntax-extensions.rst | 4 ++-- 5 files changed, 9 insertions(+), 6 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 701c62cdce..db4ebd5e38 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -656,8 +656,8 @@ changes: attribute. - Removed deprecated commands ``Arguments Scope`` and ``Implicit - Arguments`` in favor of :cmd:`Arguments`, with the help of Jasper - Hugunin. + Arguments`` in favor of :cmd:`Arguments (scopes)` and + :cmd:`Arguments (implicits)`, with the help of Jasper Hugunin. - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to avoid repeating uniform parameters in constructor declarations. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c48964d66c..2b673ff62b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1662,6 +1662,7 @@ Declaring Implicit Arguments of :token:`qualid`. .. cmd:: Arguments @qualid : clear implicits + :name: Arguments (clear implicits) This command clears implicit arguments. @@ -1738,6 +1739,7 @@ Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Arguments @qualid : default implicits + :name: Arguments (default implicits) This command tells |Coq| to automatically detect what are the implicit arguments of a defined object. @@ -1908,6 +1910,7 @@ Renaming implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Arguments @qualid {* @name} : @rename + :name: Arguments (rename) This command is used to redefine the names of implicit arguments. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 2ee23df019..cd023eb1b1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3159,7 +3159,7 @@ the conversion in hypotheses :n:`{+ @ident}`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the - ``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command. + ``/`` symbol in the argument list of the :cmd:`Arguments ` vernacular command. .. example:: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 26dc4e02cf..fa5ca81a7c 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1208,7 +1208,7 @@ Controlling the locality of commands effect of the command to the current module if the command does not occur in a section and the Global modifier extends the effect outside the current sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong + the :cmd:`Arguments `, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support extension of their scope outside sections at all and the Global modifier is not applicable to them. 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