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/proof-engine/tactics.rst | 2 +- doc/sphinx/proof-engine/vernacular-commands.rst | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/sphinx/proof-engine') 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. -- cgit v1.2.3