diff options
| author | Gaëtan Gilbert | 2019-10-28 16:02:51 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-31 14:42:54 +0100 |
| commit | ae1eb22a1365a6f477fc328eabf821fd346b5f0b (patch) | |
| tree | 9f8a2d900808f065381ad24f3d42a3be7198c6f3 | |
| parent | c67847189601cf360e9ee565ef3c1f096abd5fed (diff) | |
Doc: index command Arguments with assert
| -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) |