diff options
| author | Pierre Roux | 2020-09-08 11:53:42 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:17:09 +0200 |
| commit | 35a84b3077c219fb5f11c580a5ec405a889c0a4b (patch) | |
| tree | 4eadd0725d75695fed5235992ea682d3e4c92c7f /doc/sphinx/proof-engine | |
| parent | 5b62a6908202eef2c40d2f4989d8d21d0f6c3e16 (diff) | |
[refman] Replace num by int
num stands for natural numbers whereas the text deals with negative
values.
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 99888cbe1d..ed5de95212 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4737,12 +4737,12 @@ Non-logical tactics ------------------------ -.. tacn:: cycle @num +.. tacn:: cycle @int :name: cycle - Reorders the selected goals so that the first :n:`@num` goals appear after the + Reorders the selected goals so that the first :n:`@int` goals appear after the other selected goals. - If :n:`@num` is negative, it puts the last :n:`@num` goals at the + If :n:`@int` is negative, it puts the last :n:`@int` goals at the beginning of the list. The tactic is only useful with a goal selector, most commonly `all:`. Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent @@ -4761,11 +4761,11 @@ Non-logical tactics all: cycle 2. all: cycle -3. -.. tacn:: swap @num @num +.. tacn:: swap @int @int :name: swap Exchanges the position of the specified goals. - Negative values for :n:`@num` indicate counting goals + Negative values for :n:`@int` indicate counting goals backward from the end of the list of selected goals. Goals are indexed from 1. The tactic is only useful with a goal selector, most commonly `all:`. Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent |
