From 35a84b3077c219fb5f11c580a5ec405a889c0a4b Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 8 Sep 2020 11:53:42 +0200
Subject: [refman] Replace num by int

num stands for natural numbers whereas the text deals with negative
values.
---
 doc/sphinx/proof-engine/tactics.rst | 10 +++++-----
 1 file 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
-- 
cgit v1.2.3