[refman] Rename num to natural

1 files changed, 4 insertions, 4 deletions

diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index 3625eac4a5..738d64bfc3 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -243,16 +243,16 @@ Tactics
       Function.
 
 
-   .. tacv:: functional inversion @num
+   .. tacv:: functional inversion @natural
 
-      This does the same thing as :n:`intros until @num` followed by
+      This does the same thing as :n:`intros until @natural` followed by
       :n:`functional inversion @ident` where :token:`ident` is the
       identifier for the last introduced hypothesis.
 
    .. tacv:: functional inversion @ident @qualid
-             functional inversion @num @qualid
+             functional inversion @natural @qualid
 
-      If the hypothesis :token:`ident` (or :token:`num`) has a type of the form
+      If the hypothesis :token:`ident` (or :token:`natural`) has a type of the form
       :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where
       :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
       functional inversion, this variant allows choosing which :token:`qualid`