[refman] Rename num to natural

24 files changed, 292 insertions, 297 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index d799ecfe83..4461ff9240 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -15,10 +15,10 @@ Coq objects
 
 Our Coq domain define multiple `objects`_.  Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object).  The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise::
 
-   .. tacv:: simpl @pattern at {+ @num}
+   .. tacv:: simpl @pattern at {+ @natural}
       :name: simpl_at
 
-      This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms
+      This applies ``simpl`` only to the :n:`{+ @natural}` occurrences of the subterms
       matching :n:`@pattern` in the current goal.
 
       .. exn:: Too few occurrences
@@ -46,10 +46,10 @@ Most objects should have a body (i.e. a block of indented text following the sig
 Notations
 ---------
 
-The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax).  A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic.  The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_):
+The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax).  A typical signature might look like ``Hint Extern @natural {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``natural``), followed by an optional pattern, and a mandatory tactic.  The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_):
 
 ``@…``
-  A placeholder (``@ident``, ``@num``, ``@tactic``\ …)
+  A placeholder (``@ident``, ``@natural``, ``@tactic``\ …)
 
 ``{? …}``
   an optional block
@@ -80,9 +80,9 @@ As an exercise, what do the following patterns mean?
 
 .. code::
 
-   pattern {+, @term {? at {+ @num}}}
-   generalize {+, @term at {+ @num} as @ident}
-   fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)}
+   pattern {+, @term {? at {+ @natural}}}
+   generalize {+, @term at {+ @natural} as @ident}
+   fix @ident @natural with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)}
 
 Objects
 -------
@@ -141,7 +141,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
 ``.. opt::`` :black_nib: A Coq option (a setting with non-boolean value, e.g. a string or numeric value).
     Example::
 
-       .. opt:: Hyps Limit @num
+       .. opt:: Hyps Limit @natural
           :name Hyps Limit
 
           Controls the maximum number of hypotheses displayed in goals after
@@ -157,7 +157,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
 
     Example::
 
-        .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
+        .. prodn:: occ_switch ::= { {? {| + | - } } {* @natural } }
         term += let: @pattern := @term in @term
         | second_production
 
@@ -178,7 +178,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
 ``.. tacn::`` :black_nib: A tactic, or a tactic notation.
     Example::
 
-       .. tacn:: do @num @expr
+       .. tacn:: do @natural @expr
 
           :token:`expr` is evaluated to ``v`` which must be a tactic value. …
 
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 5762967c36..b4e21aa14a 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -15,10 +15,10 @@ Coq objects
 
 Our Coq domain define multiple `objects`_.  Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object).  The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise::
 
-   .. tacv:: simpl @pattern at {+ @num}
+   .. tacv:: simpl @pattern at {+ @natural}
       :name: simpl_at
 
-      This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms
+      This applies ``simpl`` only to the :n:`{+ @natural}` occurrences of the subterms
       matching :n:`@pattern` in the current goal.
 
       .. exn:: Too few occurrences
@@ -46,10 +46,10 @@ Most objects should have a body (i.e. a block of indented text following the sig
 Notations
 ---------
 
-The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax).  A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic.  The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_):
+The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax).  A typical signature might look like ``Hint Extern @natural {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``natural``), followed by an optional pattern, and a mandatory tactic.  The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_):
 
 ``@…``
-  A placeholder (``@ident``, ``@num``, ``@tactic``\ …)
+  A placeholder (``@ident``, ``@natural``, ``@tactic``\ …)
 
 ``{? …}``
   an optional block
@@ -80,9 +80,9 @@ As an exercise, what do the following patterns mean?
 
 .. code::
 
-   pattern {+, @term {? at {+ @num}}}
-   generalize {+, @term at {+ @num} as @ident}
-   fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)}
+   pattern {+, @term {? at {+ @natural}}}
+   generalize {+, @term at {+ @natural} as @ident}
+   fix @ident @natural with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)}
 
 Objects
 -------
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index ce68274036..c2249b8e57 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -429,11 +429,11 @@ Additional settings
 
    Provides a comment that is included at the beginning of the output files.
 
-.. opt:: Extraction Flag @num
+.. opt:: Extraction Flag @natural
    :name: Extraction Flag
 
    Controls which optimizations are used during extraction, providing a finer-grained
-   control than :flag:`Extraction Optimize`.  The bits of :token:`num` are used as a bit mask.
+   control than :flag:`Extraction Optimize`.  The bits of :token:`natural` are used as a bit mask.
    Keeping an option off keeps the extracted ML more similar to the Coq term.
    Values are:
 
diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst
index ed93145622..8a64a7ed4b 100644
--- a/doc/sphinx/addendum/nsatz.rst
+++ b/doc/sphinx/addendum/nsatz.rst
@@ -64,7 +64,7 @@ Buchberger algorithm.
 This computation is done after a step of *reification*, which is
 performed using :ref:`typeclasses`.
 
-.. tacv:: nsatz with radicalmax:=@num%N strategy:=@num%Z parameters:=[{*, @ident}] variables:=[{*, @ident}]
+.. tacv:: nsatz with radicalmax:=@natural%N strategy:=@natural%Z parameters:=[{*, @ident}] variables:=[{*, @ident}]
 
    Most complete syntax for `nsatz`.
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 3d36c5c50f..c6a4b4fe1a 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -303,9 +303,9 @@ optional tactic is replaced by the default one if not specified.
 
    Displays all remaining obligations.
 
-.. cmd:: Obligation @num {? of @ident}
+.. cmd:: Obligation @natural {? of @ident}
 
-   Start the proof of obligation :token:`num`.
+   Start the proof of obligation :token:`natural`.
 
 .. cmd:: Next Obligation {? of @ident}
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 903aa266e2..11162ec96b 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -330,7 +330,7 @@ Summary of the commands
 
          This command has no effect when used on a typeclass.
 
-.. cmd:: Instance @ident {* @binder } : @term__0 {+ @term} {? | @num} := { {*; @field_def} }
+.. cmd:: Instance @ident {* @binder } : @term__0 {+ @term} {? | @natural} := { {*; @field_def} }
 
    This command is used to declare a typeclass instance named
    :token:`ident` of the class :n:`@term__0` with parameters :token:`term` and
@@ -340,7 +340,7 @@ Summary of the commands
    An arbitrary context of :token:`binders` can be put after the name of the
    instance and before the colon to declare a parameterized instance. An
    optional priority can be declared, 0 being the highest priority as for
-   :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number
+   :tacn:`auto` hints. If the priority :token:`natural` is not specified, it defaults to the number
    of non-dependent binders of the instance.
 
    This command supports the :attr:`global` attribute that can be
@@ -362,7 +362,7 @@ Summary of the commands
       to fill them.  It works exactly as if no body had been given and
       the :tacn:`refine` tactic has been used first.
 
-   .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @num } := @term
+   .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @natural } := @term
 
       This syntax is used for declaration of singleton class instances or
       for directly giving an explicit term of type :n:`forall {* @binder }, @term__0
@@ -381,11 +381,11 @@ Summary of the commands
 Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a
 few other commands related to typeclasses.
 
-.. cmd:: Existing Instance {+ @ident} {? | @num}
+.. cmd:: Existing Instance {+ @ident} {? | @natural}
 
    This command adds an arbitrary list of constants whose type ends with
    an applied typeclass to the instance database with an optional
-   priority :token:`num`.  It can be used for redeclaring instances at the end of
+   priority :token:`natural`.  It can be used for redeclaring instances at the end of
    sections, or declaring structure projections as instances. This is
    equivalent to ``Hint Resolve ident : typeclass_instances``, except it
    registers instances for :cmd:`Print Instances`.
@@ -446,10 +446,10 @@ few other commands related to typeclasses.
    + When considering local hypotheses, we use the union of all the modes
      declared in the given databases.
 
-   .. tacv:: typeclasses eauto @num
+   .. tacv:: typeclasses eauto @natural
 
       .. warning::
-         The semantics for the limit :n:`@num`
+         The semantics for the limit :n:`@natural`
          is different than for auto. By default, if no limit is given, the
          search is unbounded. Contrary to :tacn:`auto`, introduction steps are
          counted, which might result in larger limits being necessary when
@@ -581,7 +581,7 @@ Settings
    Otherwise, the search strategy is depth-first search.  The default is off.
    :cmd:`Typeclasses eauto` is another way to set this flag.
 
-.. opt:: Typeclasses Depth @num
+.. opt:: Typeclasses Depth @natural
    :name: Typeclasses Depth
 
    Sets the maximum proof search depth.  The default is unbounded.
@@ -593,7 +593,7 @@ Settings
    also sets :opt:`Typeclasses Debug Verbosity` to 1.  :cmd:`Typeclasses eauto`
    is another way to set this flag.
 
-.. opt:: Typeclasses Debug Verbosity @num
+.. opt:: Typeclasses Debug Verbosity @natural
    :name: Typeclasses Debug Verbosity
 
    Determines how much information is shown for typeclass resolution steps during search.
@@ -604,7 +604,7 @@ Settings
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @num
+.. cmd:: Typeclasses eauto := {? debug} {? {| (dfs) | (bfs) } } @natural
    :name: Typeclasses eauto
 
    This command allows more global customization of the typeclass
@@ -618,5 +618,5 @@ Typeclasses eauto `:=`
      search (the default) or breadth-first search. The search strategy
      can also be set with :flag:`Typeclasses Iterative Deepening`.
 
-   + :token:`num` This sets the depth limit of the search. The depth
+   + :token:`natural` This sets the depth limit of the search. The depth
      limit can also be set with :opt:`Typeclasses Depth`.
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 955f48b772..fe10e345cd 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -125,7 +125,7 @@ has type :n:`@type`.
 
 .. _Axiom:
 
-.. cmd:: @assumption_token {? Inline {? ( @num ) } } {| {+ ( @assumpt ) } | @assumpt }
+.. cmd:: @assumption_token {? Inline {? ( @natural ) } } {| {+ ( @assumpt ) } | @assumpt }
    :name: Axiom; Axioms; Conjecture; Conjectures; Hypothesis; Hypotheses; Parameter; Parameters; Variable; Variables
 
    .. insertprodn assumption_token of_type
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 1f0d696d99..63c4243921 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -115,20 +115,20 @@ Numerals
   Numerals are sequences of digits with an optional fractional part
   and exponent, optionally preceded by a minus sign. Hexadecimal numerals
   start with ``0x`` or ``0X``. :n:`@int` is an integer;
-  a numeral without fractional nor exponent parts. :n:`@num` is a non-negative
+  a numeral without fractional nor exponent parts. :n:`@natural` is a non-negative
   integer.  Underscores embedded in the digits are ignored, for example
   ``1_000_000`` is the same as ``1000000``.
 
   .. insertprodn numeral hexdigit
 
   .. prodn::
-     numeral ::= {? - } @decnum {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnum }
-     | {? - } @hexnum {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnum }
-     int ::= {? - } @num
-     num ::= {| @decnum | @hexnum }
-     decnum ::= @digit {* {| @digit | _ } }
+     numeral ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat }
+     | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat }
+     int ::= {? - } @natural
+     natural ::= {| @decnat | @hexnat }
+     decnat ::= @digit {* {| @digit | _ } }
      digit ::= 0 .. 9
-     hexnum ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } }
+     hexnat ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } }
      hexdigit ::= {| 0 .. 9 | a .. f | A .. F }
 
   .. todo PR need some code fixes for hex, see PR 11948
@@ -292,7 +292,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
      .. prodn::
         document ::= {* @sentence }
         sentence ::= {? @attributes } @command .
-        | {? @attributes } {? @num : } @query_command .
+        | {? @attributes } {? @natural : } @query_command .
         | {? @attributes } {? @toplevel_selector : } @ltac_expr {| . | ... }
         | @control_command
 
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 29e703c223..866104d5d1 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -67,7 +67,7 @@ together, as well as a means of massive abstraction.
       module_binder ::= ( {? {| Import | Export } } {+ @ident } : @module_type_inl )
       module_type_inl ::= ! @module_type
       | @module_type {? @functor_app_annot }
-      functor_app_annot ::= [ inline at level @num ]
+      functor_app_annot ::= [ inline at level @natural ]
       | [ no inline ]
       module_type ::= @qualid
       | ( @module_type )
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index 0080f1d052..cd44d06e67 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -19,7 +19,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
 
    .. prodn::
       record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations }
-      record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @num } {? @decl_notations }
+      record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations }
       field_body ::= {* @binder } @of_type
       | {* @binder } @of_type := @term
       | {* @binder } := @term
diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst
index 3517d70005..98dd9a5426 100644
--- a/doc/sphinx/language/core/sorts.rst
+++ b/doc/sphinx/language/core/sorts.rst
@@ -20,7 +20,7 @@ Sorts
    | Type @%{ @universe %}
    universe ::= max ( {+, @universe_expr } )
    | @universe_expr
-   universe_expr ::= @universe_name {? + @num }
+   universe_expr ::= @universe_name {? + @natural }
 
 The types of types are called :gdef:`sorts <sort>`.
 
diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index 8e2bf32dd6..ec8e93751c 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -22,7 +22,7 @@ Variants
    :attr:`universes(noncumulative)` and :attr:`private(matching)`
    attributes.
 
-   .. exn:: The @num th argument of @ident must be @ident in @type.
+   .. exn:: The @natural th argument of @ident must be @ident in @type.
       :undocumented:
 
 Private (matching) inductive types
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 182f599a29..c36b9deef3 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -879,7 +879,7 @@ generated expression and the original.
 Here is a summary of the error messages corresponding to each
 situation:
 
-.. exn:: The constructor @ident expects @num arguments.
+.. exn:: The constructor @ident expects @natural arguments.
          The variable ident is bound several times in pattern term
          Found a constructor of inductive type term while a constructor of term is expected
 
@@ -890,8 +890,8 @@ situation:
 
    The pattern matching is not exhaustive.
 
-.. exn:: The elimination predicate term should be of arity @num (for non \
-         dependent case) or @num (for dependent case).
+.. exn:: The elimination predicate term should be of arity @natural (for non \
+         dependent case) or @natural (for dependent case).
 
    The elimination predicate provided to match has not the expected arity.
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index d8b2af092f..2bccfcd615 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -397,7 +397,7 @@ behavior.)
    `par`
       Applies :n:`@ltac_expr` to all focused goals in parallel.
       The number of workers can be controlled via the command line option
-      :n:`-async-proofs-tac-j @num` to specify the desired number of workers.
+      :n:`-async-proofs-tac-j @natural` to specify the desired number of workers.
       Limitations: ``par:`` only works on goals that don't contain existential
       variables.  :n:`@ltac_expr` must either solve the goal completely or do
       nothing (i.e. it cannot make some progress).
@@ -412,8 +412,8 @@ Selectors can also be used nested within a tactic expression with the
    .. prodn::
       selector ::= {+, @range_selector }
       | [ @ident ]
-      range_selector ::= @num - @num
-      | @num
+      range_selector ::= @natural - @natural
+      | @natural
 
    Applies :token:`ltac_expr3` to the selected goals.
 
@@ -426,10 +426,10 @@ Selectors can also be used nested within a tactic expression with the
       Limits the application of :token:`ltac_expr3` to the goal previously named :token:`ident`
       by the user (see :ref:`existential-variables`).
 
-   :n:`@num__1 - @num__2`
-      Selects the goals :n:`@num__1` through :n:`@num__2`, inclusive.
+   :n:`@natural__1 - @natural__2`
+      Selects the goals :n:`@natural__1` through :n:`@natural__2`, inclusive.
 
-   :n:`@num`
+   :n:`@natural`
       Selects a single goal.
 
 .. exn:: No such goal.
@@ -916,7 +916,7 @@ Failing
       (backtracking). If nonzero, 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 nonzero level skips the first backtrack point, even if
-      the call to :tacn:`fail` :n:`@num` is not enclosed in a :n:`+` construct,
+      the call to :tacn:`fail` :n:`@natural` is not enclosed in a :n:`+` construct,
       respecting the algebraic identity.
 
    :n:`{* {| @ident | @string | @int } }`
@@ -926,7 +926,7 @@ Failing
    .. exn:: Tactic failure.
       :undocumented:
 
-   .. exn:: Tactic failure (level @num).
+   .. exn:: Tactic failure (level @natural).
       :undocumented:
 
    .. exn:: No such goal.
@@ -976,7 +976,7 @@ amount of time:
    :name: timeout
 
    :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value
-   ``v`` is applied normally, except that it is interrupted after :n:`@num` seconds
+   ``v`` is applied normally, except that it is interrupted after :n:`@natural` seconds
    if it is still running. In this case the outcome is a failure.
 
    :tacn:`timeout` is an :token:`l3_tactic`.
@@ -1675,8 +1675,8 @@ Proving a subgoal as a separate lemma: abstract
 
    Does a :tacn:`solve` :n:`[ @ltac_expr2 ]` and saves the subproof as an auxiliary lemma.
    if :n:`@ident__name` is specified, the lemma is saved with that name; otherwise
-   the lemma is saved with the name :n:`@ident`\ `_subproof`\ :n:`{? @num }` where
-   :token:`ident` is the name of the current goal (e.g. the theorem name) and :token:`num`
+   the lemma is saved with the name :n:`@ident`\ `_subproof`\ :n:`{? @natural }` where
+   :token:`ident` is the name of the current goal (e.g. the theorem name) and :token:`natural`
    is chosen to get a fresh name.  If the proof is closed with :cmd:`Qed`, the auxiliary lemma
    is inlined in the final proof term.
 
@@ -1709,7 +1709,7 @@ Proving a subgoal as a separate lemma: abstract
 .. tacn:: transparent_abstract @ltac_expr3 {? using @ident }
 
    Like :tacn:`abstract`, but save the subproof in a transparent lemma with a name in
-   the form :n:`@ident`\ :n:`_subterm`\ :n:`{? @num }`.
+   the form :n:`@ident`\ :n:`_subterm`\ :n:`{? @natural }`.
 
    .. warning::
 
@@ -2197,7 +2197,7 @@ Backtraces
 Tracing execution
 ~~~~~~~~~~~~~~~~~
 
-.. cmd:: Info @num @ltac_expr
+.. cmd:: Info @natural @ltac_expr
 
    Applies :token:`ltac_expr` and prints a trace of the tactics that were successfully
    applied, discarding branches that failed.
@@ -2205,7 +2205,7 @@ Tracing execution
 
    This command is valid only in proof mode.  It accepts :ref:`goal-selectors`.
 
-   The number :n:`@num` is the unfolding level of tactics in the trace. At level
+   The number :n:`@natural` is the unfolding level of tactics in the trace. At level
    0, the trace contains a sequence of tactics in the actual script, at level 1,
    the trace will be the concatenation of the traces of these tactics, etc…
 
@@ -2237,12 +2237,12 @@ Tracing execution
    position in the script. In particular, the calls to idtac in branches which failed are
    not printed.
 
-   .. opt:: Info Level @num
+   .. opt:: Info Level @natural
       :name: Info Level
 
       This option is an alternative to the :cmd:`Info` command.
 
-      This will automatically print the same trace as :n:`Info @num` at each
+      This will automatically print the same trace as :n:`Info @natural` at each
       tactic call. The unfolding level can be overridden by a call to the
       :cmd:`Info` command.
 
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index b217448711..9b8749f185 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1294,7 +1294,7 @@ workarounds through Ltac1 (described below).
 
 Two examples of syntax differences:
 
-- There is no notation defined that's equivalent to :n:`intros until {| @ident | @num }`.  There is,
+- There is no notation defined that's equivalent to :n:`intros until {| @ident | @natural }`.  There is,
   however, already an ``intros_until`` tactic function defined ``Std.v``, so it may be possible for a user
   to add the necessary notation.
 - The built-in `simpl` tactic in Ltac1 supports the use of scope keys in delta flags, e.g. :n:`simpl ["+"%nat]`
@@ -1555,7 +1555,7 @@ Here is the syntax for the :n:`q_*` nonterminals:
 .. insertprodn 	ltac2_destruction_arg ltac2_constr_with_bindings
 
 .. prodn::
-   ltac2_destruction_arg ::= @num
+   ltac2_destruction_arg ::= @natural
    | @lident
    | @ltac2_constr_with_bindings
    ltac2_constr_with_bindings ::= @term {? with @ltac2_bindings }
@@ -1568,7 +1568,7 @@ Here is the syntax for the :n:`q_*` nonterminals:
    | {+ @term }
    ltac2_simple_binding ::= ( @qhyp := @term )
    qhyp ::= $ @ident
-   | @num
+   | @natural
    | @lident
 
 .. insertprodn ltac2_strategy_flag ltac2_delta_flag
@@ -1606,7 +1606,7 @@ Here is the syntax for the :n:`q_*` nonterminals:
 .. prodn::
    q_occurrences ::= {? @ltac2_occs }
    ltac2_occs ::= at @ltac2_occs_nums
-   ltac2_occs_nums ::= {? - } {+ {| @num  | $ @ident } }
+   ltac2_occs_nums ::= {? - } {+ {| @natural  | $ @ident } }
    ltac2_concl_occ ::= * {? @ltac2_occs }
    ltac2_hypident_occ ::= @ltac2_hypident {? @ltac2_occs }
    ltac2_hypident ::= @ident_or_anti
@@ -1630,7 +1630,7 @@ Here is the syntax for the :n:`q_*` nonterminals:
 
 .. prodn::
    ltac2_oriented_rewriter ::= {| -> | <- } @ltac2_rewriter
-   ltac2_rewriter ::= {? @num } {? {| ? | ! } } @ltac2_constr_with_bindings
+   ltac2_rewriter ::= {? @natural } {? {| ? | ! } } @ltac2_constr_with_bindings
 
 .. insertprodn ltac2_for_each_goal ltac2_goal_tactics
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 55e4f26fe8..f90ebadb3a 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -259,9 +259,9 @@ Name a set of section hypotheses for ``Proof using``
 
 
 
-.. cmd:: Existential @num := @term
+.. cmd:: Existential @natural := @term
 
-   This command instantiates an existential variable. :token:`num` is an index in
+   This command instantiates an existential variable. :token:`natural` is an index in
    the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`.
 
    This command is intended to be used to instantiate existential
@@ -313,9 +313,9 @@ Navigation in the proof tree
    This command cancels the effect of the last command. Thus, it
    backtracks one step.
 
-.. cmdv:: Undo @num
+.. cmdv:: Undo @natural
 
-   Repeats Undo :token:`num` times.
+   Repeats Undo :token:`natural` times.
 
 .. cmdv:: Restart
    :name: Restart
@@ -336,9 +336,9 @@ Navigation in the proof tree
 
       Prefer the use of bullets or focusing brackets (see below).
 
-.. cmdv:: Focus @num
+.. cmdv:: Focus @natural
 
-   This focuses the attention on the :token:`num` th subgoal to prove.
+   This focuses the attention on the :token:`natural` th subgoal to prove.
 
    .. deprecated:: 8.8
 
@@ -373,9 +373,9 @@ Navigation in the proof tree
    together with a suggestion about the right bullet or ``}`` to unfocus it
    or focus the next one.
 
-   .. cmdv:: @num: %{
+   .. cmdv:: @natural: %{
 
-      This focuses on the :token:`num`\-th subgoal to prove.
+      This focuses on the :token:`natural`\-th subgoal to prove.
 
    .. cmdv:: [@ident]: %{
 
@@ -439,7 +439,7 @@ Navigation in the proof tree
 
       You are trying to use ``}`` but the current subproof has not been fully solved.
 
-   .. exn:: No such goal (@num).
+   .. exn:: No such goal (@natural).
       :undocumented:
 
    .. exn:: No such goal (@ident).
@@ -559,9 +559,9 @@ Requesting information
    .. exn:: No focused proof.
       :undocumented:
 
-   .. cmdv:: Show @num
+   .. cmdv:: Show @natural
 
-      Displays only the :token:`num`\-th subgoal.
+      Displays only the :token:`natural`\-th subgoal.
 
       .. exn:: No such goal.
          :undocumented:
@@ -649,7 +649,7 @@ Requesting information
       its normalized form at the current stage of the proof, useful for
       debugging universe inconsistencies.
 
-   .. cmdv:: Show Goal @num at @num
+   .. cmdv:: Show Goal @natural at @natural
       :name: Show Goal
 
       This command is only available in coqtop.  Displays a goal at a
@@ -838,7 +838,7 @@ Controlling the effect of proof editing commands
 ------------------------------------------------
 
 
-.. opt:: Hyps Limit @num
+.. opt:: Hyps Limit @natural
    :name: Hyps Limit
 
    This option controls the maximum number of hypotheses displayed in goals
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 5a11b4f474..2d1b622a2d 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -617,7 +617,7 @@ Abbreviations
      selected occurrences of a term.
 
 .. prodn::
-   occ_switch ::= { {? {| + | - } } {* @num } }
+   occ_switch ::= { {? {| + | - } } {* @natural } }
 
 where:
 
@@ -1580,7 +1580,7 @@ whose general syntax is
    i_pattern ::= {| @ident | > | _ | ? | * | + | {? @occ_switch } {| -> | <- } | [ {?| @i_item } ] | - | [: {+ @ident } ] }
 
 .. prodn::
-   i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] }
+   i_block ::= {| [^ @ident ] | [^~ {| @ident | @natural } ] }
 
 The ``=>`` tactical first executes :token:`tactic`, then the :token:`i_item`\s,
 left to right. An :token:`s_item` specifies a
@@ -1842,8 +1842,8 @@ Block introduction
 
 :n:`[^~ @ident ]`
   *block destructing* using :token:`ident` as a suffix.
-:n:`[^~ @num ]`
-  *block destructing* using :token:`num` as a suffix.
+:n:`[^~ @natural ]`
+  *block destructing* using :token:`natural` as a suffix.
 
   Only a :token:`s_item` is allowed between the elimination tactic and
   the block destructing.
@@ -2236,17 +2236,17 @@ tactics to *permute* the subgoals generated by a tactic.
 
    These two equivalent tactics invert the order of the subgoals in focus.
 
-   .. tacv:: last @num first
+   .. tacv:: last @natural first
 
-      If :token:`num`\'s value is :math:`k`,
+      If :token:`natural`\'s value is :math:`k`,
       this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n`
       in focus. Subgoal :math:`G_{n + 1 − k}` becomes the first, and the
       circular order of subgoals remains unchanged.
 
-   .. tacn:: first @num last
+   .. tacn:: first @natural last
       :name: first (ssreflect)
 
-      If :token:`num`\'s value is :math:`k`,
+      If :token:`natural`\'s value is :math:`k`,
       this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n`
       in focus. Subgoal :math:`G_{k + 1 \bmod n}` becomes the first, and the circular order
       of subgoals remains unchanged.
@@ -2319,7 +2319,7 @@ tactic should be repeated on the current subgoal.
 There are four kinds of multipliers:
 
 .. prodn::
-   mult ::= {| @num ! | ! | @num ? | ? }
+   mult ::= {| @natural ! | ! | @natural ? | ? }
 
 Their meaning is:
 
@@ -4086,7 +4086,7 @@ will generally fail to perform congruence simplification, even on
 rather simple cases. We therefore provide a more robust alternative in
 which the function is supplied:
 
-.. tacn:: congr {? @num } @term
+.. tacn:: congr {? @natural } @term
    :name: congr
 
    This tactic:
@@ -4120,7 +4120,7 @@ which the function is supplied:
          Lemma test (x y z : nat) : x = y -> x = z.
          congr (_ = _).
 
-   The optional :token:`num` forces the number of arguments for which the
+   The optional :token:`natural` forces the number of arguments for which the
    tactic should generate equality proof obligations.
 
    This tactic supports equalities between applications with dependent
@@ -5392,8 +5392,8 @@ In this context, the identity view can be used when no view has to be applied:
 Declaring new Hint Views
 ~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Hint View for move / @ident {? | @num }
-         Hint View for apply / @ident {? | @num }
+.. cmd:: Hint View for move / @ident {? | @natural }
+         Hint View for apply / @ident {? | @natural }
 
    This command can be used to extend the database of hints for the view
    mechanism.
@@ -5410,7 +5410,7 @@ Declaring new Hint Views
    views. The optional natural number is the number of implicit
    arguments to be considered for the declared hint view lemma.
 
-   .. cmdv:: Hint View for apply//@ident {? | @num }
+   .. cmdv:: Hint View for apply//@ident {? | @natural }
 
       This variant with a double slash ``//``, declares hint views for right
       hand sides of double views.
@@ -5571,7 +5571,7 @@ Module name
 
 Natural number
 
-.. prodn:: natural ::= {| @num | @ident }
+.. prodn:: nat_or_ident ::= {| @natural | @ident }
 
 where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral
 (should not be the name of a tactic which can be followed by a
@@ -5614,19 +5614,19 @@ view :ref:`introduction_ssr`
 intro block :ref:`introduction_ssr`
 
 .. prodn::
-   i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] }
+   i_block ::= {| [^ @ident ] | [^~ {| @ident | @natural } ] }
 
 intro item  see :ref:`introduction_ssr`
 
-.. prodn:: int_mult ::= {? @num } @mult_mark
+.. prodn:: int_mult ::= {? @natural } @mult_mark
 
 multiplier  see :ref:`iteration_ssr`
 
-.. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
+.. prodn:: occ_switch ::= { {? {| + | - } } {* @natural } }
 
 occur. switch see :ref:`occurrence_selection_ssr`
 
-.. prodn:: mult ::= {? @num } @mult_mark
+.. prodn:: mult ::= {? @natural } @mult_mark
 
 multiplier see :ref:`iteration_ssr`
 
@@ -5741,7 +5741,7 @@ respectively.
 
    unlock (see :ref:`locking_ssr`)
 
-.. tacn:: congr {? @num } @term
+.. tacn:: congr {? @natural } @term
 
    congruence (see :ref:`congruence_ssr`)
 
@@ -5765,11 +5765,11 @@ localization see :ref:`localization_ssr`
 
 iteration  see :ref:`iteration_ssr`
 
-.. prodn:: tactic += @tactic ; {| first | last } {? @num } {| @tactic | [ {+| @tactic } ] }
+.. prodn:: tactic += @tactic ; {| first | last } {? @natural } {| @tactic | [ {+| @tactic } ] }
 
 selector  see :ref:`selectors_ssr`
 
-.. prodn:: tactic += @tactic ; {| first | last } {? @num }
+.. prodn:: tactic += @tactic ; {| first | last } {? @natural }
 
 rotation see :ref:`selectors_ssr`
 
@@ -5780,11 +5780,11 @@ closing see :ref:`terminators_ssr`
 Commands
 ~~~~~~~~
 
-.. cmd:: Hint View for {| move | apply } / @ident {? | @num }
+.. cmd:: Hint View for {| move | apply } / @ident {? | @natural }
 
    view hint declaration (see :ref:`declaring_new_hints_ssr`)
 
-.. cmd:: Hint View for apply // @ident {? @num }
+.. cmd:: Hint View for apply // @ident {? @natural }
 
    right hand side double , view hint declaration (see :ref:`declaring_new_hints_ssr`)
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index ed5de95212..de39edc8e9 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -100,12 +100,12 @@ The general form of a term with a bindings list is
 
   .. prodn::
      ref ::= @ident
-     | @num
+     | @natural
      bindings_list ::= {+ (@ref := @term) }
      | {+ @term }
 
 + In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an
-  :n:`@ident` or a :n:`@num`. The references are determined according to the type of
+  :n:`@ident` or a :n:`@natural`. The references are determined according to the type of
   :n:`@term`. If :n:`@ref` is an identifier, this identifier has to be bound in the
   type of :n:`@term` and the binding provides the tactic with an instance for the
   parameter of this name. If :n:`@ref` is a number ``n``, it refers to
@@ -484,7 +484,7 @@ following syntax:
      | * |- {? * {? @at_occurrences } }
      | *
      at_occurrences ::= at @occurrences
-     occurrences ::= {? - } {* @num }
+     occurrences ::= {? - } {* @natural }
 
 The role of an occurrence clause is to select a set of occurrences of a term
 in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate
@@ -921,11 +921,11 @@ Applying theorems
       This summarizes the different syntactic variants of :n:`apply @term in @ident`
       and :n:`eapply @term in @ident`.
 
-.. tacn:: constructor @num
+.. tacn:: constructor @natural
    :name: constructor
 
    This tactic applies to a goal such that its conclusion is an inductive
-   type (say :g:`I`). The argument :token:`num` must be less or equal to the
+   type (say :g:`I`). The argument :token:`natural` must be less or equal to the
    numbers of constructor(s) of :g:`I`. Let :n:`c__i` be the i-th
    constructor of :g:`I`, then :g:`constructor i` is equivalent to
    :n:`intros; apply c__i`.
@@ -942,7 +942,7 @@ Applying theorems
       :g:`constructor n` where ``n`` is the number of constructors of the head
       of the goal.
 
-   .. tacv:: constructor @num with @bindings_list
+   .. tacv:: constructor @natural with @bindings_list
 
       Let ``c`` be the i-th constructor of :g:`I`, then
       :n:`constructor i with @bindings_list` is equivalent to
@@ -1073,9 +1073,9 @@ Managing the local context
       .. exn:: No such hypothesis in current goal.
          :undocumented:
 
-   .. tacv:: intros until @num
+   .. tacv:: intros until @natural
 
-      This repeats :tacn:`intro` until the :token:`num`\-th non-dependent
+      This repeats :tacn:`intro` until the :token:`natural`\-th non-dependent
       product.
 
       .. example::
@@ -1091,7 +1091,7 @@ Managing the local context
 
       .. exn:: No such hypothesis in current goal.
 
-         This happens when :token:`num` is 0 or is greater than the number of
+         This happens when :token:`natural` is 0 or is greater than the number of
          non-dependent products of the goal.
 
    .. tacv:: intro {? @ident__1 } after @ident__2
@@ -1576,7 +1576,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
    This is equivalent to :n:`generalize @term; ... ; generalize @term`.
    Note that the sequence of term :sub:`i` 's are processed from n to 1.
 
-.. tacv:: generalize @term at {+ @num}
+.. tacv:: generalize @term at {+ @natural}
 
    This is equivalent to :n:`generalize @term` but it generalizes only over the
    specified occurrences of :n:`@term` (counting from left to right on the
@@ -1587,7 +1587,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
    This is equivalent to :n:`generalize @term` but it uses :n:`@ident` to name
    the generalized hypothesis.
 
-.. tacv:: generalize {+, @term at {+ @num} as @ident}
+.. tacv:: generalize {+, @term at {+ @natural} as @ident}
 
    This is the most general form of :n:`generalize` that combines the previous
    behaviors.
@@ -1619,16 +1619,16 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
              name the variable in the current goal and in the context of the
              existential variable. This can lead to surprising behaviors.
 
-.. tacv:: instantiate (@num := @term)
+.. tacv:: instantiate (@natural := @term)
 
    This variant allows to refer to an existential variable which was not named
-   by the user. The :n:`@num` argument is the position of the existential variable
+   by the user. The :n:`@natural` argument is the position of the existential variable
    from right to left in the goal. Because this variant is not robust to slight
    changes in the goal, its use is strongly discouraged.
 
-.. tacv:: instantiate ( @num := @term ) in @ident
-          instantiate ( @num := @term ) in ( value of @ident )
-          instantiate ( @num := @term ) in ( type of @ident )
+.. tacv:: instantiate ( @natural := @term ) in @ident
+          instantiate ( @natural := @term ) in ( value of @ident )
+          instantiate ( @natural := @term ) in ( type of @ident )
 
    These allow to refer respectively to existential variables occurring in a
    hypothesis or in the body or the type of a local definition.
@@ -1728,13 +1728,13 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as
       in :n:`destruct (@ident)`).
 
-   .. tacv:: destruct @num
+   .. tacv:: destruct @natural
 
-      :n:`destruct @num` behaves as :n:`intros until @num`
+      :n:`destruct @natural` behaves as :n:`intros until @natural`
       followed by destruct applied to the last introduced hypothesis.
 
      .. note::
-        For destruction of a numeral, use syntax :n:`destruct (@num)` (not
+        For destruction of a numeral, use syntax :n:`destruct (@natural)` (not
         very interesting anyway).
 
    .. tacv:: destruct @pattern
@@ -1827,10 +1827,10 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    This tactic behaves as :n:`intros until @ident; case @ident` when :n:`@ident`
    is a quantified variable of the goal.
 
-.. tacv:: simple destruct @num
+.. tacv:: simple destruct @natural
 
-   This tactic behaves as :n:`intros until @num; case @ident` where :n:`@ident`
-   is the name given by :n:`intros until @num` to the :n:`@num` -th
+   This tactic behaves as :n:`intros until @natural; case @ident` where :n:`@ident`
+   is the name given by :n:`intros until @natural` to the :n:`@natural` -th
    non-dependent premise of the goal.
 
 .. tacv:: case_eq @term
@@ -1861,8 +1861,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
      @ident; induction @ident`. If :n:`@ident` is not anymore dependent in the
      goal after application of :n:`induction`, it is erased (to avoid erasure,
      use parentheses, as in :n:`induction (@ident)`).
-   + If :n:`@term` is a :n:`@num`, then :n:`induction @num` behaves as
-     :n:`intros until @num` followed by :n:`induction` applied to the last
+   + If :n:`@term` is a :n:`@natural`, then :n:`induction @natural` behaves as
+     :n:`intros until @natural` followed by :n:`induction` applied to the last
      introduced hypothesis.
 
      .. note::
@@ -2024,10 +2024,10 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    This tactic behaves as :n:`intros until @ident; elim @ident` when
    :n:`@ident` is a quantified variable of the goal.
 
-.. tacv:: simple induction @num
+.. tacv:: simple induction @natural
 
-   This tactic behaves as :n:`intros until @num; elim @ident` where :n:`@ident`
-   is the name given by :n:`intros until @num` to the :n:`@num`-th non-dependent
+   This tactic behaves as :n:`intros until @natural; elim @ident` where :n:`@ident`
+   is the name given by :n:`intros until @natural` to the :n:`@natural`-th non-dependent
    premise of the goal.
 
 .. tacn:: double induction @ident @ident
@@ -2037,7 +2037,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    :n:`induction @ident; induction @ident` (or
    :n:`induction @ident ; destruct @ident` depending on the exact needs).
 
-.. tacv:: double induction @num__1 @num__2
+.. tacv:: double induction @natural__1 @natural__2
 
    This tactic is deprecated and should be replaced by
    :n:`induction num1; induction num3` where :n:`num3` is the result
@@ -2146,9 +2146,9 @@ and an explanation of the underlying technique.
 .. exn:: Not a discriminable equality.
    :undocumented:
 
-.. tacv:: discriminate @num
+.. tacv:: discriminate @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:`discriminate @ident` where :n:`@ident` is the identifier for the last
    introduced hypothesis.
 
@@ -2157,12 +2157,12 @@ and an explanation of the underlying technique.
    This does the same thing as :n:`discriminate @term` but using the given
    bindings to instantiate parameters or hypotheses of :n:`@term`.
 
-.. tacv:: ediscriminate @num
+.. tacv:: ediscriminate @natural
           ediscriminate @term {? with @bindings_list}
    :name: ediscriminate; _
 
    This works the same as :tacn:`discriminate` but if the type of :token:`term`, or the
-   type of the hypothesis referred to by :token:`num`, has uninstantiated
+   type of the hypothesis referred to by :token:`natural`, has uninstantiated
    parameters, these parameters are left as existential variables.
 
 .. tacv:: discriminate
@@ -2235,9 +2235,9 @@ and an explanation of the underlying technique.
 
       This error is given when one side of the equality is not a constructor.
 
-   .. tacv:: injection @num
+   .. tacv:: injection @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:`injection @ident` where :n:`@ident` is the identifier for the last
       introduced hypothesis.
 
@@ -2246,12 +2246,12 @@ and an explanation of the underlying technique.
       This does the same as :n:`injection @term` but using the given bindings to
       instantiate parameters or hypotheses of :n:`@term`.
 
-   .. tacv:: einjection @num
+   .. tacv:: einjection @natural
              einjection @term {? with @bindings_list}
       :name: einjection; _
 
       This works the same as :n:`injection` but if the type of :n:`@term`, or the
-      type of the hypothesis referred to by :n:`@num`, has uninstantiated
+      type of the hypothesis referred to by :n:`@natural`, has uninstantiated
       parameters, these parameters are left as existential variables.
 
    .. tacv:: injection
@@ -2263,10 +2263,10 @@ and an explanation of the underlying technique.
          :undocumented:
 
    .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern}
-             injection @num as {+ @simple_intropattern}
+             injection @natural as {+ @simple_intropattern}
              injection as {+ @simple_intropattern}
              einjection @term {? with @bindings_list} as {+ @simple_intropattern}
-             einjection @num as {+ @simple_intropattern}
+             einjection @natural as {+ @simple_intropattern}
              einjection as {+ @simple_intropattern}
 
       These variants apply :n:`intros {+ @simple_intropattern}` after the call to
@@ -2278,10 +2278,10 @@ and an explanation of the underlying technique.
       corresponds to a hypothesis.
 
    .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern
-             injection @num as @injection_intropattern
+             injection @natural as @injection_intropattern
              injection as @injection_intropattern
              einjection @term {? with @bindings_list} as @injection_intropattern
-             einjection @num as @injection_intropattern
+             einjection @natural as @injection_intropattern
              einjection as @injection_intropattern
 
       These are equivalent to the previous variants but using instead the
@@ -2330,9 +2330,9 @@ and an explanation of the underlying technique.
    :g:`Prop`). This behavior can be turned off by using the
    :flag:`Keep Proof Equalities` setting.
 
-.. tacv:: inversion @num
+.. tacv:: inversion @natural
 
-   This does the same thing as :n:`intros until @num` then :n:`inversion @ident`
+   This does the same thing as :n:`intros until @natural` then :n:`inversion @ident`
    where :n:`@ident` is the identifier for the last introduced hypothesis.
 
 .. tacv:: inversion_clear @ident
@@ -2375,9 +2375,9 @@ and an explanation of the underlying technique.
          Goal forall l:list nat, contains0 (1 :: l) -> contains0 l.
          intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ].
 
-.. tacv:: inversion @num as @or_and_intropattern_loc
+.. tacv:: inversion @natural as @or_and_intropattern_loc
 
-   This allows naming the hypotheses introduced by :n:`inversion @num` in the
+   This allows naming the hypotheses introduced by :n:`inversion @natural` in the
    context.
 
 .. tacv:: inversion_clear @ident as @or_and_intropattern_loc
@@ -2625,7 +2625,7 @@ and an explanation of the underlying technique.
 
 .. seealso:: :tacn:`functional inversion`
 
-.. tacn:: fix @ident @num
+.. tacn:: fix @ident @natural
    :name: fix
 
    This tactic is a primitive tactic to start a proof by induction. In
@@ -2633,11 +2633,11 @@ and an explanation of the underlying technique.
    as the ones described in :tacn:`induction`.
 
    In the syntax of the tactic, the identifier :n:`@ident` is the name given to
-   the induction hypothesis. The natural number :n:`@num` tells on which
+   the induction hypothesis. The natural number :n:`@natural` tells on which
    premise of the current goal the induction acts, starting from 1,
    counting both dependent and non dependent products, but skipping local
    definitions. Especially, the current lemma must be composed of at
-   least :n:`@num` products.
+   least :n:`@natural` products.
 
    Like in a fix expression, the induction hypotheses have to be used on
    structurally smaller arguments. The verification that inductive proof
@@ -2646,7 +2646,7 @@ and an explanation of the underlying technique.
    is correct at some time of the interactive development of a proof, use
    the command ``Guarded`` (see Section :ref:`requestinginformation`).
 
-.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)}
+.. tacv:: fix @ident @natural with {+ (@ident {+ @binder} [{struct @ident}] : @type)}
 
    This starts a proof by mutual induction. The statements to be simultaneously
    proved are respectively :g:`forall binder ... binder, type`.
@@ -2756,11 +2756,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
    + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many
      times as possible (perhaps zero time). This form never fails.
-   + :n:`@num?` : works similarly, except that it will do at most :token:`num` rewrites.
+   + :n:`@natural?` : works similarly, except that it will do at most :token:`natural` rewrites.
    + `!` : works as `?`, except that at least one rewrite should succeed, otherwise
      the tactic fails.
-   + :n:`@num!` (or simply :n:`@num`) : precisely :token:`num` rewrites of :token:`term` will be done,
-     leading to failure if these :token:`num` rewrites are not possible.
+   + :n:`@natural!` (or simply :n:`@natural`) : precisely :token:`natural` rewrites of :token:`term` will be done,
+     leading to failure if these :token:`natural` rewrites are not possible.
 
    .. tacv:: erewrite @term
       :name: erewrite
@@ -2937,15 +2937,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal.
       The term :n:`@term` and :n:`@term’` must be convertible.
 
-   .. tacv:: change @term at {+ @num} with @term’
+   .. tacv:: change @term at {+ @natural} with @term’
 
-      This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term` by :n:`@term’`
+      This replaces the occurrences numbered :n:`{+ @natural}` of :n:`@term` by :n:`@term’`
       in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible.
 
       .. exn:: Too few occurrences.
          :undocumented:
 
-   .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident
+   .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident
 
       This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`.
 
@@ -2990,8 +2990,8 @@ Performing computations
    | delta {? @delta_flag }
    ref_or_pattern_occ ::= @reference {? at @occs_nums }
    | @one_term {? at @occs_nums }
-   occs_nums ::= {+ {| @num | @ident } }
-   | - {| @num | @ident } {* @int_or_var }
+   occs_nums ::= {+ {| @natural | @ident } }
+   | - {| @natural | @ident } {* @int_or_var }
    int_or_var ::= @int
    | @ident
    unfold_occ ::= @reference {? at @occs_nums }
@@ -3228,9 +3228,9 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This applies :tacn:`simpl` only to the subterms matching
    :n:`@pattern` in the current goal.
 
-.. tacv:: simpl @pattern at {+ @num}
+.. tacv:: simpl @pattern at {+ @natural}
 
-   This applies :tacn:`simpl` only to the :n:`{+ @num}` occurrences of the subterms
+   This applies :tacn:`simpl` only to the :n:`{+ @natural}` occurrences of the subterms
    matching :n:`@pattern` in the current goal.
 
    .. exn:: Too few occurrences.
@@ -3243,10 +3243,10 @@ the conversion in hypotheses :n:`{+ @ident}`.
    is the unfoldable constant :n:`@qualid` (the constant can be referred to by
    its notation using :n:`@string` if such a notation exists).
 
-.. tacv:: simpl @qualid at {+ @num}
-          simpl @string at {+ @num}
+.. tacv:: simpl @qualid at {+ @natural}
+          simpl @string at {+ @natural}
 
-   This applies :tacn:`simpl` only to the :n:`{+ @num}` applicative subterms whose
+   This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose
    head occurrence is :n:`@qualid` (or :n:`@string`).
 
 .. flag:: Debug RAKAM
@@ -3374,14 +3374,14 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for
    instance, when the tactic ``apply`` fails on matching.
 
-.. tacv:: pattern @term at {+ @num}
+.. tacv:: pattern @term at {+ @natural}
 
-   Only the occurrences :n:`{+ @num}` of :n:`@term` are considered for
+   Only the occurrences :n:`{+ @natural}` of :n:`@term` are considered for
    :math:`\beta`-expansion. Occurrences are located from left to right.
 
-.. tacv:: pattern @term at - {+ @num}
+.. tacv:: pattern @term at - {+ @natural}
 
-   All occurrences except the occurrences of indexes :n:`{+ @num }`
+   All occurrences except the occurrences of indexes :n:`{+ @natural }`
    of :n:`@term` are considered for :math:`\beta`-expansion. Occurrences are located from
    left to right.
 
@@ -3394,12 +3394,12 @@ the conversion in hypotheses :n:`{+ @ident}`.
    If :g:`t`:sub:`i` occurs in one of the generated types :g:`A`:sub:`j` these
    occurrences will also be considered and possibly abstracted.
 
-.. tacv:: pattern {+, @term at {+ @num}}
+.. tacv:: pattern {+, @term at {+ @natural}}
 
-   This behaves as above but processing only the occurrences :n:`{+ @num}` of
+   This behaves as above but processing only the occurrences :n:`{+ @natural}` of
    :n:`@term` starting from :n:`@term`.
 
-.. tacv:: pattern {+, @term {? at {? -} {+, @num}}}
+.. tacv:: pattern {+, @term {? at {? -} {+, @natural}}}
 
    This is the most general syntax that combines the different variants.
 
@@ -3556,9 +3556,9 @@ Automation
       :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will
       fail even if applying manually one of the hints would succeed.
 
-   .. tacv:: auto @num
+   .. tacv:: auto @natural
 
-      Forces the search depth to be :token:`num`. The maximal search depth
+      Forces the search depth to be :token:`natural`. The maximal search depth
       is 5 by default.
 
    .. tacv:: auto with {+ @ident}
@@ -3609,7 +3609,7 @@ Automation
       Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal,
       including failing paths.
 
-   .. tacv:: {? info_}auto {? @num} {? using {+ @qualid}} {? with {+ @ident}}
+   .. tacv:: {? info_}auto {? @natural} {? using {+ @qualid}} {? with {+ @ident}}
 
       This is the most general form, combining the various options.
 
@@ -3664,7 +3664,7 @@ Automation
       Note that ``ex_intro`` should be declared as a hint.
 
 
-   .. tacv:: {? info_}eauto {? @num} {? using {+ @qualid}} {? with {+ @ident}}
+   .. tacv:: {? info_}eauto {? @natural} {? using {+ @qualid}} {? with {+ @ident}}
 
       The various options for :tacn:`eauto` are the same as for :tacn:`auto`.
 
@@ -3827,12 +3827,12 @@ automatically created.
 
       .. deprecated:: 8.10
 
-   .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident
+   .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident
       :name: Hint Resolve
 
       This command adds :n:`simple apply @qualid` to the hint list with the head
       symbol of the type of :n:`@qualid`. The cost of that hint is the number of
-      subgoals generated by :n:`simple apply @qualid` or :n:`@num` if specified. The
+      subgoals generated by :n:`simple apply @qualid` or :n:`@natural` if specified. The
       associated :n:`@pattern` is inferred from the conclusion of the type of
       :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type
       of :n:`@qualid` does not start with a product the tactic added in the hint list
@@ -3930,7 +3930,7 @@ automatically created.
       overwriting the existing settings of opacity. It is advised
       to use this just after a :cmd:`Create HintDb` command.
 
-   .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident
+   .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident
       :name: Hint Extern
 
       This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
@@ -4359,7 +4359,7 @@ some incompatibilities.
 
   This combines the effects of the different variants of :tacn:`firstorder`.
 
-.. opt:: Firstorder Depth @num
+.. opt:: Firstorder Depth @natural
    :name: Firstorder Depth
 
    This option controls the proof-search depth bound.
@@ -4396,10 +4396,10 @@ some incompatibilities.
       congruence.
       Qed.
 
-.. tacv:: congruence @num
+.. tacv:: congruence @natural
 
-  Tries to add at most :token:`num` instances of hypotheses stating quantified equalities
-  to the problem in order to solve it. A bigger value of :token:`num` does not make
+  Tries to add at most :token:`natural` instances of hypotheses stating quantified equalities
+  to the problem in order to solve it. A bigger value of :token:`natural` does not make
   success slower, only failure. You might consider adding some lemmas as
   hypotheses using assert in order for :tacn:`congruence` to use them.
 
@@ -4598,9 +4598,9 @@ symbol :g:`=`.
    then :n:`simplify_eq @ident` first introduces the hypothesis in the local
    context using :n:`intros until @ident`.
 
-.. tacv:: simplify_eq @num
+.. tacv:: simplify_eq @natural
 
-   This does the same thing as :n:`intros until @num` then
+   This does the same thing as :n:`intros until @natural` then
    :n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last
    introduced hypothesis.
 
@@ -4609,12 +4609,12 @@ symbol :g:`=`.
    This does the same as :n:`simplify_eq @term` but using the given bindings to
    instantiate parameters or hypotheses of :n:`@term`.
 
-.. tacv:: esimplify_eq @num
+.. tacv:: esimplify_eq @natural
           esimplify_eq @term {? with @bindings_list}
    :name: esimplify_eq; _
 
    This works the same as :tacn:`simplify_eq` but if the type of :n:`@term`, or the
-   type of the hypothesis referred to by :n:`@num`, has uninstantiated
+   type of the hypothesis referred to by :n:`@natural`, has uninstantiated
    parameters, these parameters are left as existential variables.
 
 .. tacv:: simplify_eq
@@ -4913,10 +4913,10 @@ Performance-oriented tactic variants
    .. tacv:: change_no_check @term with @term’
       :undocumented:
 
-   .. tacv:: change_no_check @term at {+ @num} with @term’
+   .. tacv:: change_no_check @term at {+ @natural} with @term’
       :undocumented:
 
-   .. tacv:: change_no_check @term {? {? at {+ @num}} with @term} in @ident
+   .. tacv:: change_no_check @term {? {? at {+ @natural}} with @term} in @ident
 
       .. example::
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 36ad4af837..e13558b440 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -32,7 +32,7 @@ Displaying
    .. exn:: @qualid not a defined object.
       :undocumented:
 
-   .. exn:: Universe instance should have length @num.
+   .. exn:: Universe instance should have length @natural.
       :undocumented:
 
    .. exn:: This object does not support universe names.
@@ -44,9 +44,9 @@ Displaying
    This command displays information about the current state of the
    environment, including sections and modules.
 
-.. cmd:: Inspect @num
+.. cmd:: Inspect @natural
 
-   This command displays the :n:`@num` last objects of the
+   This command displays the :n:`@natural` last objects of the
    current environment, including sections and modules.
 
 .. cmd:: Print Section @qualid
@@ -60,7 +60,7 @@ Query commands
 --------------
 
 Unlike other commands, :production:`query_command`\s may be prefixed with
-a goal selector (:n:`@num:`) to specify which goal context it applies to.
+a goal selector (:n:`@natural:`) to specify which goal context it applies to.
 If no selector is provided,
 the command applies to the current goal.  If no proof is open, then the command only applies
 to accessible objects.  (see Section :ref:`invocation-of-tactics`).
@@ -757,10 +757,10 @@ interactively, they cannot be part of a vernacular file loaded via
    of the interactive session.
 
 
-.. cmd:: Back {? @num }
+.. cmd:: Back {? @natural }
 
-   Undoes all the effects of the last :n:`@num @sentence`\s.  If
-   :n:`@num` is not specified, the command undoes one sentence.
+   Undoes all the effects of the last :n:`@natural @sentence`\s.  If
+   :n:`@natural` is not specified, the command undoes one sentence.
    Sentences read from a `.v` file via a :cmd:`Load` are considered a
    single sentence.  While :cmd:`Back` can undo tactics and commands executed
    within proof mode, once you exit proof mode, such as with :cmd:`Qed`, all
@@ -772,14 +772,14 @@ interactively, they cannot be part of a vernacular file loaded via
 
       The user wants to undo more commands than available in the history.
 
-.. cmd:: BackTo @num
+.. cmd:: BackTo @natural
 
-   This command brings back the system to the state labeled :n:`@num`,
+   This command brings back the system to the state labeled :n:`@natural`,
    forgetting the effect of all commands executed after this state. The
    state label is an integer which grows after each successful command.
    It is displayed in the prompt when in -emacs mode. Just as :cmd:`Back` (see
    above), the :cmd:`BackTo` command now handles proof states. For that, it may
-   have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if
+   have to undo some extra commands and end on a state :n:`@natural′ ≤ @natural` if
    necessary.
 
 .. _quitting-and-debugging:
@@ -834,16 +834,16 @@ Quitting and debugging
    output to the file ":n:`@string`.out".
 
 
-.. cmd:: Timeout @num @sentence
+.. cmd:: Timeout @natural @sentence
 
    Executes :n:`@sentence`. If the operation
-   has not terminated after :n:`@num` seconds, then it is interrupted and an error message is
+   has not terminated after :n:`@natural` seconds, then it is interrupted and an error message is
    displayed.
 
-   .. opt:: Default Timeout @num
+   .. opt:: Default Timeout @natural
       :name: Default Timeout
 
-      If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@num`,
+      If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@natural`,
       except for :cmd:`Timeout` commands themselves.  If unset,
       no timeout is applied.
 
@@ -890,14 +890,14 @@ Controlling display
    interpreted from left to right, so in case of an overlap, the flags on the
    right have higher priority, meaning that `A,-A` is equivalent to `-A`.
 
-.. opt:: Printing Width @num
+.. opt:: Printing Width @natural
    :name: Printing Width
 
    This command sets which left-aligned part of the width of the screen is used
    for display. At the time of writing this documentation, the default value
    is 78.
 
-.. opt:: Printing Depth @num
+.. opt:: Printing Depth @natural
    :name: Printing Depth
 
    This option controls the nesting depth of the formatter used for pretty-
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 9e8e5e5fa5..2c10e77868 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -931,7 +931,7 @@ of patterns have. The lower level is 0 and this is the level used by
 default to put rules delimited with tokens on both ends. The level is
 left to be inferred by Coq when using :n:`in custom @ident`. The
 level is otherwise given explicitly by using the syntax
-:n:`in custom @ident at level @num`, where :n:`@num` refers to the level.
+:n:`in custom @ident at level @natural`, where :n:`@natural` refers to the level.
 
 Levels are cumulative: a notation at level ``n`` of which the left end
 is a term shall use rules at level less than ``n`` to parse this
@@ -1053,8 +1053,8 @@ Here are the syntax elements used by the various notation commands.
    .. insertprodn syntax_modifier level
 
    .. prodn::
-      syntax_modifier ::= at level @num
-      | in custom @ident {? at level @num }
+      syntax_modifier ::= at level @natural
+      | in custom @ident {? at level @natural }
       | {+, @ident } at @level
       | @ident at @level {? @binder_interp }
       | @ident @explicit_subentry
@@ -1068,16 +1068,16 @@ Here are the syntax elements used by the various notation commands.
       explicit_subentry ::= ident
       | global
       | bigint
-      | strict pattern {? at level @num }
+      | strict pattern {? at level @natural }
       | binder
       | closed binder
       | constr {? at @level } {? @binder_interp }
       | custom @ident {? at @level } {? @binder_interp }
-      | pattern {? at level @num }
+      | pattern {? at level @natural }
       binder_interp ::= as ident
       | as pattern
       | as strict pattern
-      level ::= level @num
+      level ::= level @natural
       | next level
 
 .. note:: No typing of the denoted expression is performed at definition
@@ -1530,7 +1530,7 @@ numbers (see :ref:`datatypes`).
 
 .. note::
 
-   Negative integers are not at the same level as :n:`@num`, for this
+   Negative integers are not at the same level as :n:`@natural`, for this
    would make precedence unnatural.
 
 .. _numeral-notations:
@@ -1624,7 +1624,7 @@ Numeral notations
 
          .. warn:: The 'abstract after' directive has no effect when the parsing function (@qualid__parse) targets an option type.
 
-            As noted above, the :n:`(abstract after @num)` directive has no
+            As noted above, the :n:`(abstract after @natural)` directive has no
             effect when :n:`@qualid__parse` lands in an :g:`option` type.
 
    .. exn:: Cannot interpret this number as a value of type @type
@@ -1776,7 +1776,7 @@ Tactic notations allow customizing the syntax of tactics.
    can you run into problems if you shadow another tactic or tactic notation?
    If so, how to avoid ambiguity?
 
-.. cmd:: Tactic Notation {? ( at level @num ) } {+ @ltac_production_item } := @ltac_expr
+.. cmd:: Tactic Notation {? ( at level @natural ) } {+ @ltac_production_item } := @ltac_expr
 
    .. insertprodn ltac_production_item ltac_production_item
 
@@ -1789,7 +1789,7 @@ Tactic notations allow customizing the syntax of tactics.
    This command supports the :attr:`local` attribute, which limits the notation to the
    current module.
 
-      :token:`num`
+      :token:`natural`
          The parsing precedence to assign to the notation.  This information is particularly
          relevant for notations for tacticals.  Levels can be in the range 0 .. 5 (default is 5).
 
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`
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index cffe196b77..3fef3bcbd1 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -351,7 +351,7 @@ class TacticObject(NotationObject):
 
     Example::
 
-       .. tacn:: do @num @expr
+       .. tacn:: do @natural @expr
 
           :token:`expr` is evaluated to ``v`` which must be a tactic value. …
     """
@@ -401,7 +401,7 @@ class OptionObject(NotationObject):
 
     Example::
 
-       .. opt:: Hyps Limit @num
+       .. opt:: Hyps Limit @natural
           :name Hyps Limit
 
           Controls the maximum number of hypotheses displayed in goals after
@@ -452,7 +452,7 @@ class ProductionObject(CoqObject):
 
     Example::
 
-        .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
+        .. prodn:: occ_switch ::= { {? {| + | - } } {* @natural } }
         term += let: @pattern := @term in @term
         | second_production
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 549ace5d13..ff40555696 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -749,7 +749,7 @@ digit: [
 | "0" ".." "9"
 ]
 
-decnum: [
+decnat: [
 | digit LIST0 [ digit | "_" ]
 ]
 
@@ -757,26 +757,22 @@ hexdigit: [
 | [ "0" ".." "9" | "a" ".." "f" | "A" ".." "F" ]
 ]
 
-hexnum: [
+hexnat: [
 | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
 ]
 
-num: [
-| [ decnum | hexnum ]
-]
-
-natural: [ | DELETENT ]
 natural: [
-| num  (* todo: or should it be "nat"? *)
+| REPLACE bignat
+| WITH [ decnat | hexnat ]
 ]
 
 int: [
-| OPT "-" num
+| OPT "-" natural
 ]
 
 numeral: [
-| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum )
-| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum )
+| OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat )
+| OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
 ]
 
 bigint: [
@@ -1841,7 +1837,7 @@ query_command: [ ] (* re-add as a placeholder *)
 
 sentence: [
 | OPT attributes command "."
-| OPT attributes OPT ( num ":" ) query_command "."
+| OPT attributes OPT ( natural ":" ) query_command "."
 | OPT attributes OPT ( toplevel_selector ":" ) tactic_expr5 [ "." | "..." ]
 | control_command
 ]
@@ -2053,8 +2049,8 @@ tac2rec_fields: [
 
 (* todo: weird productions, ints only after an initial "-"??:
   occs_nums: [
-  | LIST1 [ num | ident ]
-  | "-" [ num | ident ] LIST0 int_or_var
+  | LIST1 [ natural | ident ]
+  | "-" [ natural | ident ] LIST0 int_or_var
 *)
 ltac2_occs_nums: [
 | DELETE LIST1 nat_or_anti      (* Ltac2 plugin *)
@@ -2160,7 +2156,7 @@ RENAME: [
 | Prim.string string
 | Prim.integer int
 | Prim.qualid qualid
-| Prim.natural num
+| Prim.natural natural
 ]
 
 gmatch_list: [
@@ -2210,7 +2206,6 @@ SPLICE: [
 | match_context_list
 | IDENT
 | LEFTQMARK
-| natural
 | NUMBER
 | STRING
 | hyp
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 3cd5a85654..6d07f6b0c4 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -130,19 +130,19 @@ type: [
 ]
 
 numeral: [
-| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum )
-| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum )
+| OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat )
+| OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
 ]
 
 int: [
-| OPT "-" num
+| OPT "-" natural
 ]
 
-num: [
-| [ decnum | hexnum ]
+natural: [
+| [ decnat | hexnat ]
 ]
 
-decnum: [
+decnat: [
 | digit LIST0 [ digit | "_" ]
 ]
 
@@ -150,7 +150,7 @@ digit: [
 | "0" ".." "9"
 ]
 
-hexnum: [
+hexnat: [
 | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
 ]
 
@@ -230,7 +230,7 @@ nonterminal: [
 
 sentence: [
 | OPT attributes command "."
-| OPT attributes OPT ( num ":" ) query_command "."
+| OPT attributes OPT ( natural ":" ) query_command "."
 | OPT attributes OPT ( toplevel_selector ":" ) ltac_expr [ "." | "..." ]
 | control_command
 ]
@@ -277,7 +277,7 @@ universe: [
 ]
 
 universe_expr: [
-| universe_name OPT ( "+" num )
+| universe_name OPT ( "+" natural )
 ]
 
 universe_name: [
@@ -509,8 +509,8 @@ ref_or_pattern_occ: [
 ]
 
 occs_nums: [
-| LIST1 [ num | ident ]
-| "-" [ num | ident ] LIST0 int_or_var
+| LIST1 [ natural | ident ]
+| "-" [ natural | ident ] LIST0 int_or_var
 ]
 
 int_or_var: [
@@ -535,7 +535,7 @@ record_definition: [
 ]
 
 record_field: [
-| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) name OPT field_body OPT [ "|" natural ] OPT decl_notations
 ]
 
 field_body: [
@@ -589,7 +589,7 @@ sort_family: [
 ]
 
 hint_info: [
-| "|" OPT num OPT one_term
+| "|" OPT natural OPT one_term
 ]
 
 module_binder: [
@@ -602,7 +602,7 @@ module_type_inl: [
 ]
 
 functor_app_annot: [
-| "[" "inline" "at" "level" num "]"
+| "[" "inline" "at" "level" natural "]"
 | "[" "no" "inline" "]"
 ]
 
@@ -714,7 +714,7 @@ command: [
 | "Locate" reference
 | "Locate" "Term" reference
 | "Locate" "Module" qualid
-| "Info" num ltac_expr
+| "Info" natural ltac_expr
 | "Locate" "Ltac" qualid
 | "Locate" "Library" qualid
 | "Locate" "File" string
@@ -762,7 +762,7 @@ command: [
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
 | "Print" "Namespace" dirpath
-| "Inspect" num
+| "Inspect" natural
 | "Add" "ML" "Path" string
 | OPT "Export" "Set" setting_name
 | "Print" "Table" setting_name
@@ -773,7 +773,7 @@ command: [
 | "Restore" "State" [ ident | string ]
 | "Reset" "Initial"
 | "Reset" ident
-| "Back" OPT num
+| "Back" OPT natural
 | "Debug" [ "On" | "Off" ]
 | "Declare" "Reduction" ident ":=" red_expr
 | "Declare" "Custom" "Entry" ident
@@ -802,17 +802,17 @@ command: [
 | "Proof" "Mode" string
 | "Proof" term
 | "Abort" OPT [ "All" | ident ]
-| "Existential" num OPT ( ":" term ) ":=" term
+| "Existential" natural OPT ( ":" term ) ":=" term
 | "Admitted"
 | "Qed"
 | "Save" ident
 | "Defined" OPT ident
 | "Restart"
-| "Undo" OPT ( OPT "To" num )
-| "Focus" OPT num
+| "Undo" OPT ( OPT "To" natural )
+| "Focus" OPT natural
 | "Unfocus"
 | "Unfocused"
-| "Show" OPT [ ident | num ]
+| "Show" OPT [ ident | natural ]
 | "Show" "Existentials"
 | "Show" "Universes"
 | "Show" "Conjectures"
@@ -824,7 +824,7 @@ command: [
 | "Create" "HintDb" ident OPT "discriminated"
 | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
 | "Hint" hint OPT ( ":" LIST1 ident )
-| "Comments" LIST0 [ one_term | string | num ]
+| "Comments" LIST0 [ one_term | string | natural ]
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
 | "Declare" "Scope" scope_name
 | "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
@@ -894,7 +894,7 @@ command: [
 | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT int
 | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
 | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
-| "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr
+| "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
 | "Ltac" tacdef_body LIST0 ( "with" tacdef_body )
@@ -916,7 +916,7 @@ command: [
 | "String" "Notation" qualid qualid qualid ":" scope_name
 | "SubClass" ident_decl def_body
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
-| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
+| assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
 | [ "Definition" | "Example" ] ident_decl def_body
 | "Let" ident_decl def_body
 | "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
@@ -959,7 +959,7 @@ command: [
 | "Context" LIST1 binder
 | "Instance" OPT ( ident_decl LIST0 binder ) ":" term OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ]
 | "Existing" "Instance" qualid OPT hint_info
-| "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
+| "Existing" "Instances" LIST1 qualid OPT [ "|" natural ]
 | "Existing" "Class" qualid
 | "Arguments" reference LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ]
 | "Implicit" [ "Type" | "Types" ] reserv_list
@@ -995,12 +995,12 @@ command: [
 | "Print" "Ltac2" qualid      (* Ltac2 plugin *)
 | "Time" sentence
 | "Redirect" string sentence
-| "Timeout" num sentence
+| "Timeout" natural sentence
 | "Fail" sentence
 | "Drop"
 | "Quit"
-| "BackTo" num
-| "Show" "Goal" num "at" num
+| "BackTo" natural
+| "Show" "Goal" natural "at" natural
 ]
 
 section_subset_expr: [
@@ -1067,8 +1067,8 @@ univ_name_list: [
 
 hint: [
 | "Resolve" LIST1 [ qualid | one_term ] OPT hint_info
-| "Resolve" "->" LIST1 qualid OPT num
-| "Resolve" "<-" LIST1 qualid OPT num
+| "Resolve" "->" LIST1 qualid OPT natural
+| "Resolve" "<-" LIST1 qualid OPT natural
 | "Immediate" LIST1 [ qualid | one_term ]
 | "Variables" "Transparent"
 | "Variables" "Opaque"
@@ -1079,7 +1079,7 @@ hint: [
 | "Mode" qualid LIST1 [ "+" | "!" | "-" ]
 | "Unfold" LIST1 qualid
 | "Constructors" LIST1 qualid
-| "Extern" num OPT one_term "=>" ltac_expr
+| "Extern" natural OPT one_term "=>" ltac_expr
 ]
 
 tacdef_body: [
@@ -1127,7 +1127,7 @@ lident: [
 ]
 
 destruction_arg: [
-| num
+| natural
 | constr_with_bindings
 | constr_with_bindings_arg
 ]
@@ -1221,7 +1221,7 @@ q_destruction_arg: [
 ]
 
 ltac2_destruction_arg: [
-| num      (* Ltac2 plugin *)
+| natural      (* Ltac2 plugin *)
 | lident      (* Ltac2 plugin *)
 | ltac2_constr_with_bindings      (* Ltac2 plugin *)
 ]
@@ -1249,7 +1249,7 @@ ltac2_simple_binding: [
 
 qhyp: [
 | "$" ident      (* Ltac2 plugin *)
-| num      (* Ltac2 plugin *)
+| natural      (* Ltac2 plugin *)
 | lident      (* Ltac2 plugin *)
 ]
 
@@ -1318,8 +1318,8 @@ class: [
 ]
 
 syntax_modifier: [
-| "at" "level" num
-| "in" "custom" ident OPT ( "at" "level" num )
+| "at" "level" natural
+| "in" "custom" ident OPT ( "at" "level" natural )
 | LIST1 ident SEP "," "at" level
 | ident "at" level OPT binder_interp
 | ident explicit_subentry
@@ -1336,12 +1336,12 @@ explicit_subentry: [
 | "ident"
 | "global"
 | "bigint"
-| "strict" "pattern" OPT ( "at" "level" num )
+| "strict" "pattern" OPT ( "at" "level" natural )
 | "binder"
 | "closed" "binder"
 | "constr" OPT ( "at" level ) OPT binder_interp
 | "custom" ident OPT ( "at" level ) OPT binder_interp
-| "pattern" OPT ( "at" "level" num )
+| "pattern" OPT ( "at" "level" natural )
 ]
 
 binder_interp: [
@@ -1351,7 +1351,7 @@ binder_interp: [
 ]
 
 level: [
-| "level" num
+| "level" natural
 | "next" "level"
 ]
 
@@ -1388,14 +1388,14 @@ simple_tactic: [
 | "esplit" OPT ( "with" bindings )
 | "exists" OPT ( LIST1 bindings SEP "," )
 | "eexists" OPT ( LIST1 bindings SEP "," )
-| "intros" "until" [ ident | num ]
+| "intros" "until" [ ident | natural ]
 | "intro" OPT ident OPT where
 | "move" ident OPT where
 | "rename" LIST1 ( ident "into" ident ) SEP ","
 | "revert" LIST1 ident
-| "simple" "induction" [ ident | num ]
-| "simple" "destruct" [ ident | num ]
-| "double" "induction" [ ident | num ] [ ident | num ]
+| "simple" "induction" [ ident | natural ]
+| "simple" "destruct" [ ident | natural ]
+| "double" "induction" [ ident | natural ] [ ident | natural ]
 | "admit"
 | "clear" LIST0 ident
 | "clear" "-" LIST1 ident
@@ -1551,7 +1551,7 @@ simple_tactic: [
 | "eelim" constr_with_bindings_arg OPT ( "using" constr_with_bindings )
 | "case" induction_clause_list
 | "ecase" induction_clause_list
-| "fix" ident num OPT ( "with" LIST1 fixdecl )
+| "fix" ident natural OPT ( "with" LIST1 fixdecl )
 | "cofix" ident OPT ( "with" LIST1 cofixdecl )
 | "pose" bindings_with_parameters
 | "pose" one_term OPT as_name
@@ -1585,11 +1585,11 @@ simple_tactic: [
 | "edestruct" induction_clause_list
 | "rewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
 | "erewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
-| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | num ] OPT as_or_and_ipat OPT [ "with" one_term ]
-| "simple" "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
-| "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
-| "inversion_clear" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
-| "inversion" [ ident | num ] "using" one_term OPT ( "in" LIST1 ident )
+| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | natural ] OPT as_or_and_ipat OPT [ "with" one_term ]
+| "simple" "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
+| "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
+| "inversion_clear" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
+| "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident )
 | "red" OPT clause_dft_concl
 | "hnf" OPT clause_dft_concl
 | "simpl" OPT delta_flag OPT ref_or_pattern_occ OPT clause_dft_concl
@@ -1610,7 +1610,7 @@ simple_tactic: [
 | "f_equal"
 | "firstorder" OPT ltac_expr firstorder_rhs
 | "gintuition" OPT ltac_expr
-| "functional" "inversion" [ ident | num ] OPT qualid      (* funind plugin *)
+| "functional" "inversion" [ ident | natural ] OPT qualid      (* funind plugin *)
 | "functional" "induction" term OPT fun_ind_using OPT with_names      (* funind plugin *)
 | "soft" "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names      (* funind plugin *)
 | "psatz_Z" OPT int_or_var ltac_expr
@@ -1698,7 +1698,7 @@ as_name: [
 ]
 
 rewriter: [
-| OPT num OPT [ "?" | "!" ] constr_with_bindings_arg
+| OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg
 ]
 
 oriented_rewriter: [
@@ -1758,7 +1758,7 @@ simple_intropattern_closed: [
 
 simple_binding: [
 | "(" ident ":=" term ")"
-| "(" num ":=" term ")"
+| "(" natural ":=" term ")"
 ]
 
 bindings: [
@@ -1807,7 +1807,7 @@ ltac2_occs: [
 ]
 
 ltac2_occs_nums: [
-| OPT "-" LIST1 [ num      (* Ltac2 plugin *) | "$" ident ]      (* Ltac2 plugin *)
+| OPT "-" LIST1 [ natural      (* Ltac2 plugin *) | "$" ident ]      (* Ltac2 plugin *)
 ]
 
 ltac2_concl_occ: [
@@ -1858,7 +1858,7 @@ ltac2_oriented_rewriter: [
 ]
 
 ltac2_rewriter: [
-| OPT num OPT [ "?" | "!" ] ltac2_constr_with_bindings
+| OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings
 ]
 
 q_dispatch: [
@@ -2328,8 +2328,8 @@ selector: [
 ]
 
 range_selector: [
-| num "-" num
-| num
+| natural "-" natural
+| natural
 ]
 
 match_key: [