[sphinx] Replace remaining `@natural` by `@num`.

2 files changed, 10 insertions, 10 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 86b178290..dc9add66f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -547,7 +547,7 @@ Failing
    :tacn:`fail` tactic will, however, succeed if all the goals have already been
    solved.
 
-   .. tacv:: fail @natural
+   .. tacv:: fail @num
 
       The number is the failure level. If no level is specified, it defaults to 0.
       The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching
@@ -555,14 +555,14 @@ Failing
       (backtracking). If non zero, the current :tacn:`match goal` block, :tacn:`try`,
       :tacn:`repeat`, or branching command is aborted and the level is decremented. In
       the case of :n:`+`, a non-zero level skips the first backtrack point, even if
-      the call to :n:`fail @natural` is not enclosed in a :n:`+` command,
+      the call to :n:`fail @num` is not enclosed in a :n:`+` command,
       respecting the algebraic identity.
 
    .. tacv:: fail {* message_token}
 
       The given tokens are used for printing the failure message.
 
-   .. tacv:: fail @natural {* message_token}
+   .. tacv:: fail @num {* message_token}
 
       This is a combination of the previous variants.
 
@@ -573,7 +573,7 @@ Failing
 
    .. tacv:: gfail {* message_token}
 
-   .. tacv:: gfail @natural {* message_token}
+   .. tacv:: gfail @num {* message_token}
 
       These variants fail with an error message or an error level even if
       there are no goals left. Be careful however if Coq terms have to be
@@ -581,7 +581,7 @@ Failing
       tactic into the goals, meaning that if there are no goals when it is
       evaluated, a tactic call like :n:`let x:=H in fail 0 x` will succeed.
 
-   .. exn:: Tactic Failure message (level @natural).
+   .. exn:: Tactic Failure message (level @num).
 
 Timeout
 ~~~~~~~
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 977a5b8fa..8816c934a 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2157,10 +2157,10 @@ equivalent to:
 
 More generally, the tactic:
 
-.. tacn:: @tactic; last @natural first
+.. tacn:: @tactic; last @num first
    :name: last first
 
-where :token:`natural` is a |Coq| numeral, or and Ltac variable
+where :token:`num` is a |Coq| numeral, or an Ltac variable
 denoting a |Coq|
 numeral, having the value k. It rotates the n subgoals G1 , …, Gn
 generated by tactic. The first subgoal becomes Gn + 1 − k and the
@@ -2168,7 +2168,7 @@ circular order of subgoals remains unchanged.
 
 Conversely, the tactic:
 
-.. tacn:: @tactic; first @natural last
+.. tacn:: @tactic; first @num last
    :name: first last
 
 rotates the n subgoals G1 , …, Gn generated by tactic in order that
@@ -5322,11 +5322,11 @@ intro item  see :ref:`introduction_ssr`
 
 multiplier  see :ref:`iteration_ssr`
 
-.. prodn:: occ_switch ::= { {? + %| - } {* @natural } }
+.. prodn:: occ_switch ::= { {? + %| - } {* @num } }
 
 occur. switch see :ref:`occurrence_selection_ssr`
 
-.. prodn:: mult ::= {? @natural } @mult_mark
+.. prodn:: mult ::= {? @num } @mult_mark
 
 multiplier see :ref:`iteration_ssr`