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, 23 insertions, 22 deletions

diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
index 595934ad89..c7e3999691 100644
--- a/theories/Numbers/AltBinNotations.v
+++ b/theories/Numbers/AltBinNotations.v
@@ -1,34 +1,35 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** * Alternative Binary Numeral Notations *)
 
 (** Faster but less safe parsers and printers of [positive], [N], [Z]. *)
 
-(** Nowadays, literals in types [positive], [N], [Z] are parsed and
+(** By default, literals in types [positive], [N], [Z] are parsed and
     printed via the [Numeral Notation] command, by conversion from/to
-    the [Decimal.int] representation. This way, we do not need any
-    ML library of arbitrary precision integers (bigint.ml), hence
-    reducing the amount of ML code to trust during parsing and printing.
-    But this new method is slower than the older code, by a margin that
-    may become significant for literals of thousands of digits and more.
-    If that becomes a problem for your development, this file provides
-    some alternative [Numeral Notation] commmands that use [Z] as
-    bridge type : it hence relies on the bigint.ml library, the efficiency
-    should be almost the one of the legacy code, at the expense of a
-    larger ML trust base. To enable these commands, just be sure to
-    [Require] this file after the other files of
-
-    Please note anyway that literals above 10000 digits in [positive],
-    [N], [Z] will end up triggering Stack Overlow in various parts of
-    the Coq engine (type-checker, reduction, etc). So consider using
-    [BigN] or [BigZ] instead...
-*)
+    the [Decimal.int] representation. When working with numbers with
+    thousands of digits and more, conversion from/to [Decimal.int] can
+    become significantly slow. If that becomes a problem for your
+    development, this file provides some alternative [Numeral
+    Notation] commmands that use [Z] as bridge type. To enable these
+    commands, just be sure to [Require] this file after other files
+    defining numeral notations.
+
+    Note: up to Coq 8.8, literals in types [positive], [N], [Z] were
+    parsed and printed using a native ML library of arbitrary
+    precision integers named bigint.ml. From 8.9, the default is to
+    parse and print using a Coq library converting sequences of
+    digits, hence reducing the amount of ML code to trust. But this
+    method is slower. This file then gives access to the legacy
+    method, trading efficiency against a larger ML trust base relying
+    on bigint.ml. *)
 
 Require Import BinNums.