Fix numeral notation for a rebase on top of master

Some of this code is cargo-culted or kludged to work.

As I understand it, the situation is as follows:
There are two sorts of use-cases that need to be supported:
1. A plugin registers an OCaml function as a numeral interpreter.  In
   this case, the function registration must be synchronized with the
   document state, but the functions should not be marshelled / stored
   in the .vo.
2. A vernacular registers a Gallina function as a numeral interpreter.
   In this case, the registration must be synchronized, and the function
   should be marshelled / stored in the .vo.

In case (1), we can compare functions by pointer equality, and we should
be able to rely on globally unique keys, even across backtracking.

In case (2), we cannot compare functions by pointer equality (because
they must be regenerated on unmarshelling when `Require`ing a .vo file),
and we also cannot rely on any sort of unique key being both unique and
persistent across files.

The solution we use here is that we ask clients to provide "unique"
keys, and that clients tell us whether or not to overwrite existing
registered functions, i.e., to tell us whether or not we should expect
interpreter functions to be globally unique under pointer equality.  For
plugins, a simple string suffices, as long as the string does not clash
between different plugins.  In the case of vernacular-registered
functions, use marshell a description of all of the data used to
generate the function, and use that string as a unique key which is
expected to persist across files.  Because we cannot rely on
function-pointer uniqueness here, we tell the
interpretation-registration to allow overwriting.

----

Some of this code is response to comments on the PR

----

Some code is to fix an issue that bignums revealed:

Both Int31 and bignums registered numeral notations in int31_scope.  We
now prepend a globally unique identifier when registering numeral
notations from OCaml plugins.  This is permissible because we don't
store the uid information for such notations in .vo files (assuming I'm
understanding the code correctly).

1 files changed, 124 insertions, 36 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index e947fd891b..ca588acf29 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1379,42 +1379,130 @@ Numeral notations
 Starting with version 8.9, the following command allows the user to customize
 the way numeral literals are parsed and printed:
 
-.. cmd:: Numeral Notation @ty @pa @pr : @scope.
-
-In the previous line, `ty` should be the name of an inductive type,
-while `pa` and `pr` should be the names of two parsing and printing
-functions.
-The parsing function `pa` should have one of the following types:
-
-  * :g:`Decimal.int -> ty`
-  * :g:`Decimal.int -> option ty`
-  * :g:`Decimal.uint -> ty`
-  * :g:`Decimal.uint -> option ty`
-  * :g:`Z -> ty`
-  * :g:`Z -> option ty`
-
-And the printing function `pr` should have one of the following types:
-
-  * :g:`ty -> Decimal.int`
-  * :g:`ty -> option Decimal.int`
-  * :g:`ty -> Decimal.uint`
-  * :g:`ty -> option Decimal.uint`
-  * :g:`ty -> Z`
-  * :g:`ty -> option Z`
-
-.. cmdv:: Numeral Notation @ty @pa @pr : @scope (warning after @n).
-
-When a literal larger than `n` is parsed, a warning message about
-possible stack overflow will be displayed.
-
-.. cmdv:: Numeral Notation @ty @pa @pr : @scope (abstract after @n).
-
-When a literal `m` larger than `n` is parsed, the result will be
-:g:`(pa m)`, without reduction of this application to a normal form.
-Here `m` will be a ``Decimal.int`` or ``Decimal.uint`` or ``Z``,
-depending on the type of the parsing function `pa`. This allows a more
-compact representation of literals in types such as ``nat``, and
-limits parse failures due to stack overflow.
+.. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope.
+
+  In the previous line, :n:`@ident__1` should be the name of an
+  inductive type, while :n:`@ident__2` and :n:`@ident__3` should be
+  the names of the parsing and printing functions, respectively.  The
+  parsing function :n:`@ident__2` should have one of the following
+  types:
+
+    * :n:`Decimal.int -> @ident__1`
+    * :n:`Decimal.int -> option @ident__1`
+    * :n:`Decimal.uint -> @ident__1`
+    * :n:`Decimal.uint -> option @ident__1`
+    * :n:`Z -> @ident__1`
+    * :n:`Z -> option @ident__1`
+
+  And the printing function :n:`@ident__3` should have one of the
+  following types:
+
+    * :n:`@ident__1 -> Decimal.int`
+    * :n:`@ident__1 -> option Decimal.int`
+    * :n:`@ident__1 -> Decimal.uint`
+    * :n:`@ident__1 -> option Decimal.uint`
+    * :n:`@ident__1 -> Z`
+    * :n:`@ident__1 -> option Z`
+
+  .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num).
+
+    When a literal larger than :token:`num` is parsed, a warning
+    message about possible stack overflow, resulting from evaluating
+    :n:`@ident__2`, will be displayed.
+
+  .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num).
+
+    When a literal :g:`m` larger than :token:`num` is parsed, the
+    result will be :n:`(@ident__2 m)`, without reduction of this
+    application to a normal form.  Here :g:`m` will be a
+    :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the
+    type of the parsing function :n:`@ident__2`. 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:`num`
+    is parsed.
+
+  .. exn:: Cannot interpret this number as a value of type @type
+
+    The numeral notation registered for :g:`ty` does not support the
+    given numeral.  This error is given when the interpretation
+    function returns :g:`None`, or if the interpretation is registered
+    for only non-negative integers, and the given numeral is negative.
+
+  .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}.
+
+    The parsing function given to the :cmd:`Numeral Notation`
+    vernacular is not of the right type.
+
+  .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int).  Instead of Decimal.int, the the types Decimal.uint or Z could be used{? (require BinNums first)}.
+
+    The printing function given to the :cmd:`Numeral Notation`
+    vernacular is not of the right type.
+
+  .. exn:: @type is not an inductive type
+
+    Numeral notations can only be declared for inductive types with no
+    arguments.
+
+  .. exn:: The inductive type @type cannot be used in numeral notations because support for polymorphic inductive types is not yet implemented.
+
+    Numeral notations do not currently support polymorphic inductive
+    types.  Ensure that all types involved in numeral notations are
+    declared with :g:`Unset Universe Polymorphism`, or with the
+    :g:`Monomorphic` attribute.
+
+  .. exn:: The function @ident cannot be used in numeral notations because support for polymorphic printing and parsing functions is not yet implemented.
+
+    Numeral notations do not currently support polymorphic functions
+    for printing and parsing.  Ensure that both functions passed to
+    :cmd:`Numeral Notation` are defined with :g:`Unset Universe
+    Polymorphism`, or with the :g:`Monomorphic` attribute.
+
+  .. exn:: Unexpected term while parsing a numeral notation
+
+    Parsing functions must always return ground terms, made up of
+    applications of constructors and inductive types.  Parsing
+    functions may not return terms containing axioms, bare
+    (co)fixpoints, lambdas, etc.
+
+  .. exn:: Unexpected non-option term while parsing a numeral notation
+
+    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 decimal.  They may not return
+    opaque constants.
+
+  .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]).
+
+    The type passed to :cmd:`Numeral Notation` must be a single
+    identifier.
+
+  .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]).
+
+    Both functions passed to :cmd:`Numeral Notation` must be single
+    identifiers.
+
+  .. 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 @num)`, this warning is emitted when
+    parsing a numeral greater than or equal to :token:`num`.
+
+  .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2.
+
+    When a :cmd:`Numeral Notation` is registered in the current scope
+    with :n:`(abstract after @num)`, this warning is emitted when
+    parsing a numeral greater than or equal to :token:`num`.
+    Typically, this indicates that the fully computed representation
+    of numerals can be so large that non-tail-recursive OCaml
+    functions run out of stack space when trying to walk them.
+
+    For example
+
+    .. coqtop:: all
+
+       Check 90000.
+
 
 .. _TacticNotation: