diff options
| author | Emilio Jesus Gallego Arias | 2019-10-31 20:41:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-31 20:41:30 +0100 |
| commit | 151b84a3540d1972d53460780396f2749d0378cf (patch) | |
| tree | 42a1d2b0784d83f489dc043f57cf9482056ab501 /doc/sphinx | |
| parent | bc70919118fe5450c3bb798632d64823659f4814 (diff) | |
| parent | 85905b38c15c3d2bb73e878e6e7db180b73d468e (diff) | |
Merge PR #10985: Print argument info as an Arguments command in About
Ack-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: ejgallego
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f477bf239d..f50cf9340c 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1927,9 +1927,11 @@ Renaming implicit arguments This command is used to redefine the names of implicit arguments. -With the assert flag, ``Arguments`` can be used to assert that a given -object has the expected number of arguments and that these arguments -are named as expected. +.. cmd:: Arguments @qualid {* @name} : assert + :name: Arguments (assert) + + This command is used to assert that a given object has the expected + number of arguments and that these arguments are named as expected. .. example:: (continued) |