diff options
| author | Pierre Roux | 2020-09-07 11:53:49 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:20:28 +0200 |
| commit | 724966f56caa66a5ddc9a992cf870ebc2efae004 (patch) | |
| tree | 53954c47fd9e400d1e6006d38472c0b858893303 /doc/sphinx/user-extensions | |
| parent | 754e138e1e1c86dcd5e9d07084a5d33a5056ce9d (diff) | |
[refman] Rename int to integer
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 8474d0287f..d31ec51d52 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1887,7 +1887,7 @@ Tactic notations allow customizing the syntax of tactics. - :tacn:`refine` * - ``integer`` - - :token:`int` + - :token:`integer` - an integer - |