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).

6 files changed, 272 insertions, 113 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:
 
diff --git a/interp/notation.ml b/interp/notation.ml
index f60ddcf909..56d6acbdae 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -378,38 +378,39 @@ let prim_token_interp_infos =
 let prim_token_uninterp_infos =
   ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t)
 
-let hashtbl_check_and_set uid f h eq =
+let hashtbl_check_and_set allow_overwrite uid f h eq =
   match Hashtbl.find h uid with
    | exception Not_found -> Hashtbl.add h uid f
+   | _ when allow_overwrite -> Hashtbl.add h uid f
    | g when eq f g -> ()
    | _ ->
       user_err ~hdr:"prim_token_interpreter"
        (str "Unique identifier " ++ str uid ++
         str " already used to register a numeral or string (un)interpreter.")
 
-let register_gen_interpretation uid (interp, uninterp) =
+let register_gen_interpretation allow_overwrite uid (interp, uninterp) =
   hashtbl_check_and_set
-    uid interp prim_token_interpreters InnerPrimToken.interp_eq;
+    allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq;
   hashtbl_check_and_set
-    uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
+    allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
 
-let register_rawnumeral_interpretation uid (interp, uninterp) =
-  register_gen_interpretation uid
+let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+  register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp)
 
-let register_bignumeral_interpretation uid (interp, uninterp) =
-  register_gen_interpretation uid
+let register_bignumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+  register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp)
 
-let register_string_interpretation uid (interp, uninterp) =
-  register_gen_interpretation uid
+let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+  register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp)
 
 type prim_token_infos = {
   pt_scope : scope_name; (** Concerned scope *)
   pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
   pt_required : required_module; (** Module that should be loaded first *)
-  pt_refs : global_reference list; (** Entry points during uninterpretation *)
+  pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
   pt_in_match : bool (** Is this prim token legal in match patterns ? *)
 }
 
@@ -445,19 +446,25 @@ let enable_prim_token_interpretation infos =
     (the latter inside a [Mltop.declare_cache_obj]).
 *)
 
+let fresh_string_of =
+  let count = ref 0 in
+  fun root -> count := !count+1; (string_of_int !count)^"_"^root
+
 let declare_numeral_interpreter sc dir interp (patl,uninterp,b) =
-  register_bignumeral_interpretation sc (interp,uninterp);
+  let uid = fresh_string_of sc in
+  register_bignumeral_interpretation uid (interp,uninterp);
   enable_prim_token_interpretation
     { pt_scope = sc;
-      pt_uid = sc;
+      pt_uid = uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }
 let declare_string_interpreter sc dir interp (patl,uninterp,b) =
-  register_string_interpretation sc (interp,uninterp);
+  let uid = fresh_string_of sc in
+  register_string_interpretation uid (interp,uninterp);
   enable_prim_token_interpretation
     { pt_scope = sc;
-      pt_uid = sc;
+      pt_uid = uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }
diff --git a/interp/notation.mli b/interp/notation.mli
index 2545e494ef..1d01d75c82 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -91,19 +91,19 @@ type 'a prim_token_interpretation =
   'a prim_token_interpreter * 'a prim_token_uninterpreter
 
 val register_rawnumeral_interpretation :
-  prim_token_uid -> rawnum prim_token_interpretation -> unit
+  ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit
 
 val register_bignumeral_interpretation :
-  prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit
+  ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit
 
 val register_string_interpretation :
-  prim_token_uid -> string prim_token_interpretation -> unit
+  ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
 
 type prim_token_infos = {
   pt_scope : scope_name; (** Concerned scope *)
   pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
   pt_required : required_module; (** Module that should be loaded first *)
-  pt_refs : global_reference list; (** Entry points during uninterpretation *)
+  pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
   pt_in_match : bool (** Is this prim token legal in match patterns ? *)
 }
 
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index caba4db4fc..19a15fd1df 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  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)         *)
 (************************************************************************)
 
 DECLARE PLUGIN "numeral_notation_plugin"
@@ -16,7 +18,6 @@ open Globnames
 open Constrexpr
 open Constrexpr_ops
 open Constr
-open Misctypes
 
 (** * Numeral notation *)
 
@@ -24,7 +25,7 @@ open Misctypes
 
     The constr [c] below isn't necessarily well-typed, since we
     built it via an [mkApp] of a conversion function on a term
-    that starts with the right constructor, but might be partially
+    that starts with the right constructor but might be partially
     applied.
 
     At least [c] is known to be evar-free, since it comes from
@@ -55,7 +56,7 @@ let warn_large_num =
   CWarnings.create ~name:"large-number" ~category:"numbers"
     (fun ty ->
       strbrk "Stack overflow or segmentation fault happens when " ++
-      strbrk "working with large numbers in " ++ pr_reference ty ++
+      strbrk "working with large numbers in " ++ pr_qualid ty ++
       strbrk " (threshold may vary depending" ++
       strbrk " on your system limits and on the command executed).")
 
@@ -64,11 +65,11 @@ let warn_abstract_large_num =
     (fun (ty,f) ->
       let (sigma, env) = Pfedit.get_current_context () in
       strbrk "To avoid stack overflow, large numbers in " ++
-      pr_reference ty ++ strbrk " are interpreted as applications of " ++
+      pr_qualid ty ++ strbrk " are interpreted as applications of " ++
       Printer.pr_constr_env env sigma f ++ strbrk ".")
 
 (** Comparing two raw numbers (base 10, big-endian, non-negative).
-    A bit nasty, but not critical : only used to decide when a
+    A bit nasty, but not critical: only used to decide when a
     number is considered as large (see warnings above). *)
 
 exception Comp of int
@@ -233,18 +234,24 @@ let rec glob_of_constr ?loc c = match Constr.kind c with
   | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
   | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
   | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
-  | _ -> CErrors.anomaly (str "Numeral.interp: unexpected constr")
+  | _ -> let (sigma, env) = Pfedit.get_current_context () in
+         CErrors.user_err ?loc
+          (str "Unexpected term while parsing a numeral notation:" ++ fnl () ++
+           Printer.pr_constr_env env sigma c)
 
 let no_such_number ?loc ty =
   CErrors.user_err ?loc
    (str "Cannot interpret this number as a value of type " ++
-    pr_reference ty)
+    pr_qualid ty)
 
 let interp_option ty ?loc c =
   match Constr.kind c with
   | App (_Some, [| _; c |]) -> glob_of_constr ?loc c
   | App (_None, [| _ |]) -> no_such_number ?loc ty
-  | x -> CErrors.anomaly (str "Numeral.interp: option expected")
+  | x -> let (sigma, env) = Pfedit.get_current_context () in
+         CErrors.user_err ?loc
+          (str "Unexpected non-option term while parsing a numeral notation:" ++ fnl () ++
+           Printer.pr_constr_env env sigma c)
 
 let uninterp_option c =
   match Constr.kind c with
@@ -276,7 +283,7 @@ type numeral_notation_obj =
     to_ty : constr;
     of_kind : conversion_kind;
     of_ty : constr;
-    num_ty : Libnames.reference; (* for warnings / error messages *)
+    num_ty : Libnames.qualid; (* for warnings / error messages *)
     warning : numnot_option }
 
 let interp o ?loc n =
@@ -322,7 +329,7 @@ let uninterp o (Glob_term.AnyGlobConstr n) =
 
 let load_numeral_notation _ (_, (uid,opts)) =
   Notation.register_rawnumeral_interpretation
-    uid (interp opts, uninterp opts)
+    ~allow_overwrite:true uid (interp opts, uninterp opts)
 
 let cache_numeral_notation x = load_numeral_notation 1 x
 
@@ -355,7 +362,7 @@ let unsafe_locate_ind q =
 
 let locate_ind q =
   try unsafe_locate_ind q
-  with Not_found -> Nametab.error_global_not_found (CAst.make q)
+  with Not_found -> Nametab.error_global_not_found q
 
 let locate_z () =
   try
@@ -367,35 +374,33 @@ let locate_int () =
   { uint = locate_ind q_uint;
     int = locate_ind q_int }
 
-let locate_globref r =
-  let q = qualid_of_reference r in
-  try Nametab.locate CAst.(q.v)
+let locate_globref q =
+  try Nametab.locate q
   with Not_found -> Nametab.error_global_not_found q
 
-let locate_constant r =
-  let q = qualid_of_reference r in
-  try Nametab.locate_constant CAst.(q.v)
+let locate_constant q =
+  try Nametab.locate_constant q
   with Not_found -> Nametab.error_global_not_found q
 
 let has_type f ty =
   let (sigma, env) = Pfedit.get_current_context () in
-  let c = mkCastC (mkRefC f, CastConv ty) in
+  let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
   try let _ = Constrintern.interp_constr env sigma c in true
   with Pretype_errors.PretypeError _ -> false
 
 let type_error_to f ty loadZ =
   CErrors.user_err
-    (pr_reference f ++ str " should go from Decimal.int to " ++
-     pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")." ++
-     fnl () ++ str "Instead of int, the types uint or Z could be used" ++
-     (if loadZ then str " (load Z first)." else str "."))
+    (pr_qualid f ++ str " should go from Decimal.int to " ++
+     pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
+     fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++
+     (if loadZ then str " (require BinNums first)." else str "."))
 
 let type_error_of g ty loadZ =
   CErrors.user_err
-    (pr_reference g ++ str " should go from " ++ pr_reference ty ++
-     str " to Decimal.int or (option int)." ++ fnl () ++
-     str "Instead of int, the types uint or Z could be used" ++
-     (if loadZ then str " (load Z first)." else str "."))
+    (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
+     str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
+     str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++
+     (if loadZ then str " (require BinNums first)." else str "."))
 
 let vernac_numeral_notation ty f g scope opts =
   let int_ty = locate_int () in
@@ -405,7 +410,7 @@ let vernac_numeral_notation ty f g scope opts =
   let of_ty = mkConst (locate_constant g) in
   let cty = mkRefC ty in
   let app x y = mkAppC (x,[y]) in
-  let cref q = mkRefC (CAst.make (Qualid q)) in
+  let cref q = mkRefC q in
   let arrow x y =
     mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
   in
@@ -420,17 +425,20 @@ let vernac_numeral_notation ty f g scope opts =
        get_constructors ind
     | IndRef _ ->
        CErrors.user_err
-         (str "The inductive type " ++ pr_reference ty ++
-          str " cannot be polymorphic here for the moment")
+         (str "The inductive type " ++ pr_qualid ty ++
+          str " cannot be used in numeral notations because" ++
+          str " support for polymorphic inductive types is not yet implemented")
     | ConstRef _ | ConstructRef _ | VarRef _ ->
        CErrors.user_err
-        (pr_reference ty ++ str " is not an inductive type")
+        (pr_qualid ty ++ str " is not an inductive type")
   in
   (* Check the type of f *)
   let to_kind =
     if Global.is_polymorphic (Nametab.global f) then
       CErrors.user_err
-        (pr_reference f ++ str " cannot be polymorphic for the moment")
+        (str "The function " ++ pr_qualid f ++ str " cannot be used" ++
+         str " in numeral notations because support for polymorphic" ++
+         str " printing and parsing functions is not yet implemented.")
     else if has_type f (arrow cint cty) then Int int_ty, Direct
     else if has_type f (arrow cint (opt cty)) then Int int_ty, Option
     else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct
@@ -447,7 +455,7 @@ let vernac_numeral_notation ty f g scope opts =
   let of_kind =
     if Global.is_polymorphic (Nametab.global g) then
       CErrors.user_err
-        (pr_reference g ++ str " cannot be polymorphic for the moment")
+        (pr_qualid g ++ str " cannot be polymorphic for the moment")
     else if has_type g (arrow cty cint) then Int int_ty, Direct
     else if has_type g (arrow cty (opt cint)) then Int int_ty, Option
     else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct
diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
new file mode 100644
index 0000000000..a06327c5e6
--- /dev/null
+++ b/test-suite/success/NumeralNotations.v
@@ -0,0 +1,55 @@
+
+(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *)
+
+(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *)
+Module Test1.
+  Axiom hold : forall {A B C}, A -> B -> C.
+  Definition opaque3 (x : Decimal.int) : Decimal.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end).
+  Numeral Notation Decimal.int opaque3 opaque3 : opaque_scope.
+  Delimit Scope opaque_scope with opaque.
+  Fail Check 1%opaque.
+End Test1.
+
+(* https://github.com/coq/coq/pull/8064#discussion_r202497990 *)
+Module Test2.
+  Axiom opaque4 : option Decimal.int.
+  Definition opaque6 (x : Decimal.int) : option Decimal.int := opaque4.
+  Numeral Notation Decimal.int opaque6 opaque6 : opaque_scope.
+  Delimit Scope opaque_scope with opaque.
+  Open Scope opaque_scope.
+  Fail Check 1%opaque.
+End Test2.
+
+Module Test3.
+  Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A).
+  Definition to_silly (v : Decimal.uint) := SILLY v (fun _ x => x).
+  Definition of_silly (v : silly) := match v with SILLY v _ => v end.
+  Numeral Notation silly to_silly of_silly : silly_scope.
+  Delimit Scope silly_scope with silly.
+  Fail Check 1%silly.
+End Test3.
+
+
+Module Test4.
+  Polymorphic Inductive punit := ptt.
+  Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end.
+  Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0.
+  Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end.
+  Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0.
+  Polymorphic Definition pto_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end.
+  Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
+  Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end.
+  Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
+  Fail Numeral Notation punit to_punit of_punit : pto.
+  Fail Numeral Notation punit pto_punit of_punit : ppo.
+  Fail Numeral Notation punit to_punit pof_punit : ptp.
+  Fail Numeral Notation punit pto_punit pof_punit : ppp.
+  Numeral Notation unit to_unit of_unit : uto.
+  Delimit Scope uto with uto.
+  Check let v := 0%uto in v : unit.
+  Fail Check 1%uto.
+  Fail Check (-1)%uto.
+  Fail Numeral Notation unit pto_unit of_unit : upo.
+  Fail Numeral Notation unit to_unit pof_unit : utp.
+  Fail Numeral Notation unit pto_unit pof_unit : upp.
+End Test4.
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.