[refman] Rename num to natural

7 files changed, 16 insertions, 16 deletions

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.