aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
diff options
context:
space:
mode:
authorPierre Roux2020-09-08 11:53:42 +0200
committerPierre Roux2020-09-11 22:17:09 +0200
commit35a84b3077c219fb5f11c580a5ec405a889c0a4b (patch)
tree4eadd0725d75695fed5235992ea682d3e4c92c7f /doc/sphinx/proof-engine
parent5b62a6908202eef2c40d2f4989d8d21d0f6c3e16 (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.rst10
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