[refman] Explicit integer and natural

As respectively bigint and bignat that fit into an OCaml int.

4 files changed, 33 insertions, 23 deletions

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index d248839fa0..9308da6d27 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -114,9 +114,9 @@ Identifiers
 Numbers
   Numbers 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 number without fractional nor exponent parts. :n:`@natural` is a non-negative
-  integer.  Underscores embedded in the digits are ignored, for example
+  start with ``0x`` or ``0X``. :n:`@bigint` are integers;
+  numbers without fractional nor exponent parts. :n:`@bignat` are non-negative
+  integers.  Underscores embedded in the digits are ignored, for example
   ``1_000_000`` is the same as ``1000000``.
 
   .. insertprodn number hexdigit
@@ -125,13 +125,17 @@ Numbers
      number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat }
      | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat }
      integer ::= {? - } @natural
-     natural ::= {| @decnat | @hexnat }
+     natural ::= @bignat
+     bigint ::= {? - } @bignat
+     bignat ::= {| @decnat | @hexnat }
      decnat ::= @digit {* {| @digit | _ } }
      digit ::= 0 .. 9
      hexnat ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } }
      hexdigit ::= {| 0 .. 9 | a .. f | A .. F }
 
-  .. todo PR need some code fixes for hex, see PR 11948
+  :n:`@integer` and :n:`@natural` are limited to the range that fits
+  into an OCaml integer (63-bit integers on most architectures).
+  :n:`@bigint` and :n:`@bignat` have no range limitation.
 
 Strings
   Strings begin and end with ``"`` (double quote).  Use ``""`` to represent
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index d31ec51d52..e8b1add95e 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1544,8 +1544,8 @@ Numeral notations
    .. insertprodn numeral_modifier numeral_modifier
 
    .. prodn::
-      numeral_modifier ::= ( warning after @number )
-      | ( abstract after @number )
+      numeral_modifier ::= ( warning after @bignat )
+      | ( abstract after @bignat )
 
    This command allows the user to customize the way numeral literals
    are parsed and printed.
@@ -1591,33 +1591,33 @@ Numeral notations
          function application, constructors, inductive type families,
          sorts, and primitive integers) will be considered for printing.
 
-      :n:`( warning after @number )`
+      :n:`( warning after @bignat )`
          displays a warning message about a possible stack
-         overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@number`.
+         overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@bignat`.
 
          .. 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 @number)`, this warning is emitted when
-            parsing a number greater than or equal to :token:`number`.
+            with :n:`(warning after @bignat)`, this warning is emitted when
+            parsing a number greater than or equal to :token:`bignat`.
 
-      :n:`( abstract after @number )`
+      :n:`( abstract after @bignat )`
          returns :n:`(@qualid__parse m)` when parsing a literal
-         :n:`m` that's greater than :n:`@number` rather than reducing it to a normal form.
+         :n:`m` that's greater than :n:`@bignat` 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:`number`
-         is parsed.  Note that :n:`(abstract after @number)` has no effect
+         warning will be emitted when an integer larger than :token:`bignat`
+         is parsed.  Note that :n:`(abstract after @bignat)` 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 @number)`, this warning is emitted when
-            parsing a number greater than or equal to :token:`number`.
+            with :n:`(abstract after @bignat)`, this warning is emitted when
+            parsing a number greater than or equal to :token:`bignat`.
             Typically, this indicates that the fully computed representation
             of numbers can be so large that non-tail-recursive OCaml
             functions run out of stack space when trying to walk them.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 89009764c8..ea60fa22d6 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -756,8 +756,8 @@ hexnat: [
 | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
 ]
 
-natural: [
-| REPLACE bignat
+bignat: [
+| REPLACE NUMBER
 | WITH [ decnat | hexnat ]
 ]
 
@@ -2197,7 +2197,6 @@ ltac2_induction_clause: [
 SPLICE: [
 | clause
 | noedit_mode
-| bigint
 | match_list
 | match_context_list
 | IDENT
@@ -2360,7 +2359,6 @@ SPLICE: [
 | search_queries
 | locatable
 | scope_delimiter
-| bignat
 | one_import_filter_name
 | search_where
 | message_token
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 105bd4668e..8d4e0189e6 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -139,6 +139,14 @@ integer: [
 ]
 
 natural: [
+| bignat
+]
+
+bigint: [
+| OPT "-" bignat
+]
+
+bignat: [
 | [ decnat | hexnat ]
 ]
 
@@ -1291,8 +1299,8 @@ field_mod: [
 ]
 
 numeral_modifier: [
-| "(" "warning" "after" number ")"
-| "(" "abstract" "after" number ")"
+| "(" "warning" "after" bignat ")"
+| "(" "abstract" "after" bignat ")"
 ]
 
 hints_path: [