[refman] Rename numeral to number

6 files changed, 39 insertions, 39 deletions

diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index c27eb216e8..765373619f 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -1062,7 +1062,7 @@ Floating-point constants are parsed and pretty-printed as (17-digit)
 decimal constants. This ensures that the composition
 :math:`\text{parse} \circ \text{print}` amounts to the identity.
 
-.. warn:: The constant @numeral is not a binary64 floating-point value.  A closest value @numeral will be used and unambiguously printed @numeral. [inexact-float,parsing]
+.. warn:: The constant @number is not a binary64 floating-point value.  A closest value @number will be used and unambiguously printed @number. [inexact-float,parsing]
 
    Not all decimal constants are floating-point values. This warning
    is generated when parsing such a constant (for instance ``0.1``).
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 63c4243921..be513833ad 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -119,10 +119,10 @@ Numerals
   integer.  Underscores embedded in the digits are ignored, for example
   ``1_000_000`` is the same as ``1000000``.
 
-  .. insertprodn numeral hexdigit
+  .. insertprodn number hexdigit
 
   .. prodn::
-     numeral ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat }
+     number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat }
      | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat }
      int ::= {? - } @natural
      natural ::= {| @decnat | @hexnat }
diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index ec8e93751c..2904250e41 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -79,7 +79,7 @@ to apply specific treatments accordingly.
    | %{%| {* @qualid := @pattern } %|%}
    | _
    | ( {+| @pattern } )
-   | @numeral
+   | @number
    | @string
 
 Note that the :n:`@pattern ::= @pattern10 : @term` production
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 2c10e77868..8474d0287f 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1124,7 +1124,7 @@ refer to different definitions depending on which notation scopes
 are currently open.  For instance, the infix symbol ``+`` can be
 used to refer to distinct definitions of the addition operator,
 such as for natural numbers, integers or reals.
-Notation scopes can include an interpretation for numerals and
+Notation scopes can include an interpretation for numbers and
 strings with the :cmd:`Numeral Notation` and :cmd:`String Notation` commands.
 
    .. insertprodn scope scope_key
@@ -1311,31 +1311,31 @@ Scopes` or :cmd:`Print Scope`.
 
 ``nat_scope``
   This scope includes the standard arithmetical operators and relations on type
-  nat. Positive integer numerals in this scope are mapped to their canonical
+  nat. Positive integer numbers in this scope are mapped to their canonical
   representent built from :g:`O` and :g:`S`. The scope is delimited by the key
   ``nat``, and bound to the type :g:`nat` (see above).
 
 ``N_scope``
   This scope includes the standard arithmetical operators and relations on
   type :g:`N` (binary natural numbers). It is delimited by the key ``N`` and comes
-  with an interpretation for numerals as closed terms of type :g:`N`.
+  with an interpretation for numbers as closed terms of type :g:`N`.
 
 ``Z_scope``
   This scope includes the standard arithmetical operators and relations on
   type :g:`Z` (binary integer numbers). It is delimited by the key ``Z`` and comes
-  with an interpretation for numerals as closed terms of type :g:`Z`.
+  with an interpretation for numbers as closed terms of type :g:`Z`.
 
 ``positive_scope``
   This scope includes the standard arithmetical operators and relations on
   type :g:`positive` (binary strictly positive numbers). It is delimited by
-  key ``positive`` and comes with an interpretation for numerals as closed
+  key ``positive`` and comes with an interpretation for numbers as closed
   terms of type :g:`positive`.
 
 ``Q_scope``
   This scope includes the standard arithmetical operators and relations on
   type :g:`Q` (rational numbers defined as fractions of an integer and a
   strictly positive integer modulo the equality of the numerator-
-  denominator cross-product) and comes with an interpretation for numerals
+  denominator cross-product) and comes with an interpretation for numbers
   as closed terms of type :g:`Q`.
 
 ``Qc_scope``
@@ -1346,7 +1346,7 @@ Scopes` or :cmd:`Print Scope`.
 ``R_scope``
   This scope includes the standard arithmetical operators and relations on
   type :g:`R` (axiomatic real numbers). It is delimited by the key ``R`` and comes
-  with an interpretation for numerals using the :g:`IZR` morphism from binary
+  with an interpretation for numbers using the :g:`IZR` morphism from binary
   integer numbers to :g:`R` and :g:`Z.pow_pos` for potential exponent parts.
 
 ``bool_scope``
@@ -1514,18 +1514,18 @@ Abbreviations
 
 .. extracted from Gallina chapter
 
-Numerals and strings
---------------------
+Numbers and strings
+-------------------
 
 .. insertprodn primitive_notations primitive_notations
 
 .. prodn::
-   primitive_notations ::= @numeral
+   primitive_notations ::= @number
    | @string
 
-Numerals and strings have no predefined semantics in the calculus. They are
+Numbers and strings have no predefined semantics in the calculus. They are
 merely notations that can be bound to objects through the notation mechanism.
-Initially, numerals are bound to Peano’s representation of natural
+Initially, numbers are bound to Peano’s representation of natural
 numbers (see :ref:`datatypes`).
 
 .. note::
@@ -1544,8 +1544,8 @@ Numeral notations
    .. insertprodn numeral_modifier numeral_modifier
 
    .. prodn::
-      numeral_modifier ::= ( warning after @numeral )
-      | ( abstract after @numeral )
+      numeral_modifier ::= ( warning after @number )
+      | ( abstract after @number )
 
    This command allows the user to customize the way numeral literals
    are parsed and printed.
@@ -1591,35 +1591,35 @@ Numeral notations
          function application, constructors, inductive type families,
          sorts, and primitive integers) will be considered for printing.
 
-      :n:`( warning after @numeral )`
+      :n:`( warning after @number )`
          displays a warning message about a possible stack
-         overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@numeral`.
+         overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@number`.
 
          .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed).
 
             When a :cmd:`Numeral Notation` is registered in the current scope
-            with :n:`(warning after @numeral)`, this warning is emitted when
-            parsing a numeral greater than or equal to :token:`numeral`.
+            with :n:`(warning after @number)`, this warning is emitted when
+            parsing a number greater than or equal to :token:`number`.
 
-      :n:`( abstract after @numeral )`
+      :n:`( abstract after @number )`
          returns :n:`(@qualid__parse m)` when parsing a literal
-         :n:`m` that's greater than :n:`@numeral` rather than reducing it to a normal form.
+         :n:`m` that's greater than :n:`@number` rather than reducing it to a normal form.
          Here :g:`m` will be a
          :g:`Numeral.int` or :g:`Numeral.uint` or :g:`Z`, depending on the
          type of the parsing function :n:`@qualid__parse`. This allows for a
          more compact representation of literals in types such as :g:`nat`,
          and limits parse failures due to stack overflow.  Note that a
-         warning will be emitted when an integer larger than :token:`numeral`
-         is parsed.  Note that :n:`(abstract after @numeral)` has no effect
+         warning will be emitted when an integer larger than :token:`number`
+         is parsed.  Note that :n:`(abstract after @number)` has no effect
          when :n:`@qualid__parse` lands in an :g:`option` type.
 
          .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @qualid__parse.
 
             When a :cmd:`Numeral Notation` is registered in the current scope
-            with :n:`(abstract after @numeral)`, this warning is emitted when
-            parsing a numeral greater than or equal to :token:`numeral`.
+            with :n:`(abstract after @number)`, this warning is emitted when
+            parsing a number greater than or equal to :token:`number`.
             Typically, this indicates that the fully computed representation
-            of numerals can be so large that non-tail-recursive OCaml
+            of numbers can be so large that non-tail-recursive OCaml
             functions run out of stack space when trying to walk them.
 
          .. warn:: The 'abstract after' directive has no effect when the parsing function (@qualid__parse) targets an option type.
@@ -1630,9 +1630,9 @@ Numeral notations
    .. exn:: Cannot interpret this number as a value of type @type
 
      The numeral notation registered for :token:`type` does not support
-     the given numeral.  This error is given when the interpretation
+     the given number.  This error is given when the interpretation
      function returns :g:`None`, or if the interpretation is registered
-     only for integers or non-negative integers, and the given numeral
+     only for integers or non-negative integers, and the given number
      has a fractional or exponent part or is negative.
 
 
@@ -1657,7 +1657,7 @@ Numeral notations
 
      Parsing functions expected to return an :g:`option` must always
      return a concrete :g:`Some` or :g:`None` when applied to a
-     concrete numeral expressed as a (hexa)decimal.  They may not return
+     concrete number expressed as a (hexa)decimal.  They may not return
      opaque constants.
 
 String notations
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index ff40555696..fbf83760ad 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -770,7 +770,7 @@ int: [
 | OPT "-" natural
 ]
 
-numeral: [
+number: [
 | OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat )
 | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
 ]
@@ -795,7 +795,7 @@ ident: [
 ]
 
 NUMBER: [
-| numeral
+| number
 ]
 
 (* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 6d07f6b0c4..a021bdbec0 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -93,7 +93,7 @@ term_explicit: [
 ]
 
 primitive_notations: [
-| numeral
+| number
 | string
 ]
 
@@ -129,7 +129,7 @@ type: [
 | term
 ]
 
-numeral: [
+number: [
 | OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat )
 | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
 ]
@@ -429,7 +429,7 @@ pattern0: [
 | "{|" LIST0 ( qualid ":=" pattern ) "|}"
 | "_"
 | "(" LIST1 pattern SEP "|" ")"
-| numeral
+| number
 | string
 ]
 
@@ -1291,8 +1291,8 @@ field_mod: [
 ]
 
 numeral_modifier: [
-| "(" "warning" "after" numeral ")"
-| "(" "abstract" "after" numeral ")"
+| "(" "warning" "after" number ")"
+| "(" "abstract" "after" number ")"
 ]
 
 hints_path: [