Merge PR #8064: Numeral notation (revisited again)

48 files changed, 1605 insertions, 537 deletions

diff --git a/CHANGES b/CHANGES
index a42c44c09b..5d1c9a9c2d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -65,6 +65,33 @@ Standard Library
 
 - Added `Ndigits.N2Bv_sized`, and proved some lemmas about it.
 
+- The scopes `int_scope` and `uint_scope` have been renamed to
+  `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect
+  and other packages.  They are still delimited by `%int` and `%uint`.
+
+- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`,
+  and `int31` are no longer available merely by `Require`ing the files
+  that define the inductives.  You must `Import` `Coq.Strings.String`,
+  `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
+  `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and
+  `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use
+  these notations.  Note that passing `-compat 8.8` or issuing
+  `Require Import Coq.Compat.Coq88` will make these notations
+  available.  Users wishing to port their developments automatically
+  may download `fix.py` from
+  <https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169>
+  and run a command like `while true; do make -Okj 2>&1 |
+  /path/to/fix.py; done` and get a cup of coffee.  (This command must
+  be manually interrupted once the build finishes all the way though.
+  Note also that this method is not fail-proof; you may have to adjust
+  some scopes if you were relying on string notations not being
+  available even when `string_scope` was open.)
+
+- Numeral syntax for `nat` is no longer available without loading the
+  entire prelude (`Require Import Coq.Init.Prelude`).  This only
+  impacts users running Coq without the init library (`-nois` or
+  `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
@@ -98,6 +125,8 @@ Vernacular Commands
   overwritting the opacity set of the hint database.
 - Added generic syntax for “attributes”, as in:
   `#[local] Lemma foo : bar.`
+- Added the `Numeral Notation` command for registering decimal numeral
+  notations for custom types
 - The `Set SsrHave NoTCResolution` command no longer has special global
   scope. If you want the previous behavior, use `Global Set SsrHave
   NoTCResolution`.
diff --git a/Makefile.common b/Makefile.common
index 772561bd70..09457ced7b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -140,13 +140,12 @@ FOCMO:=plugins/firstorder/ground_plugin.cmo
 CCCMO:=plugins/cc/cc_plugin.cmo
 BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo
 RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
-NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo
-OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
-        positive_syntax_plugin.cmo n_syntax_plugin.cmo \
-        z_syntax_plugin.cmo r_syntax_plugin.cmo \
+SYNTAXCMO:=$(addprefix plugins/syntax/, \
+        r_syntax_plugin.cmo \
 	int31_syntax_plugin.cmo \
 	ascii_syntax_plugin.cmo \
-        string_syntax_plugin.cmo )
+        string_syntax_plugin.cmo \
+	numeral_notation_plugin.cmo)
 DERIVECMO:=plugins/derive/derive_plugin.cmo
 LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
@@ -156,7 +155,7 @@ PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
         $(QUOTECMO) $(RINGCMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
-        $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
+        $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
 	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh
new file mode 100644
index 0000000000..76aa37d380
--- /dev/null
+++ b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh
@@ -0,0 +1,5 @@
+if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then
+    HoTT_CI_REF=fix-for-numeral-notations
+    HoTT_CI_GITURL=https://github.com/JasonGross/HoTT
+    HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive
+fi
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 5089a1b3e3..b46382dbbf 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1372,6 +1372,154 @@ Abbreviations
    denoted expression is performed at definition time. Type checking is
    done only at the time of use of the abbreviation.
 
+
+Numeral notations
+-----------------
+
+.. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope.
+
+  This command allows the user to customize the way numeral literals
+  are parsed and printed.
+
+  The token :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`
+
+    When parsing, the application of the parsing function
+    :n:`@ident__2` to the number will be fully reduced, and universes
+    of the resulting term will be refreshed.
+
+  .. 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.  Note that :n:`(abstract after @num)` has no effect
+    when :n:`@ident__2` lands in an :g:`option` type.
+
+  .. 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
+    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 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:: Unexpected term @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 @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:: Cannot interpret in @scope because @ident could not be found in the current environment.
+
+    The inductive type used to register the numeral notation is no
+    longer available in the environment.  Most likely, this is because
+    the numeral notation was declared inside a functor for an
+    inductive type inside the functor.  This use case is not currently
+    supported.
+
+    Alternatively, you might be trying to use a primitive token
+    notation from a plugin which forgot to specify which module you
+    must :g:`Require` for access to that notation.
+
+  .. 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.
+
+  .. exn:: The reference @ident was not found in the current environment.
+
+    Identifiers passed to :cmd:`Numeral Notation` must exist in the
+    global environment.
+
+  .. exn:: @ident is bound to a notation that does not denote a reference.
+
+    Identifiers passed to :cmd:`Numeral Notation` must be global
+    references, or notations which denote to 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.
+
+  .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type.
+
+    As noted above, the :n:`(abstract after @num)` directive has no
+    effect when :n:`@ident__2` lands in an :g:`option` type.
+
 .. _TacticNotation:
 
 Tactic Notations
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index f448248468..0fa42cadad 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -226,6 +226,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/BinNums.v
     theories/Numbers/NumPrelude.v
     theories/Numbers/NaryFunctions.v
+    theories/Numbers/AltBinNotations.v
     theories/Numbers/DecimalFacts.v
     theories/Numbers/DecimalNat.v
     theories/Numbers/DecimalPos.v
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 009894fddb..ddc0a5c000 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -531,18 +531,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   else
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
-      let (sc,p) = uninterp_prim_token_ind_pattern ind args in
-      match availability_of_entry_coercion custom InConstrEntrySomeLevel with
-        | None -> raise No_match
-        | Some coercion ->
-      match availability_of_prim_token p sc scopes with
-	| None -> raise No_match
-	| Some key ->
-          insert_pat_coercion coercion (insert_pat_delimiters (CAst.make @@ CPatPrim p) key)
-    with No_match ->
-      try
-	if !Flags.raw_print || !print_no_symbol then raise No_match;
-        extern_notation_ind_pattern allscopes vars ind args
+      extern_notation_ind_pattern allscopes vars ind args
           (uninterp_ind_pattern_notations ind)
     with No_match ->
       let c = extern_reference vars (IndRef ind) in
diff --git a/interp/notation.ml b/interp/notation.ml
index 625d072b9f..55ead946cb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -266,16 +266,14 @@ let keymap_find key map =
 (* Scopes table : interpretation -> scope_name *)
 let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
 
-let prim_token_key_table = ref (KeyMap.empty : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t)
-
 let glob_prim_constr_key c = match DAst.get c with
-  | GRef (ref, _) -> RefKey (canonical_gr ref)
+  | GRef (ref, _) -> Some (canonical_gr ref)
   | GApp (c, _) ->
     begin match DAst.get c with
-    | GRef (ref, _) -> RefKey (canonical_gr ref)
-    | _ -> Oth
+    | GRef (ref, _) -> Some (canonical_gr ref)
+    | _ -> None
     end
-  | _ -> Oth
+  | _ -> None
 
 let glob_constr_keys c = match DAst.get c with
   | GApp (c, _) ->
@@ -303,77 +301,189 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
 (* Interpreting numbers (not in summary because functional objects)   *)
 
 type required_module = full_path * string list
+type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
 
-type 'a prim_token_interpreter =
-    ?loc:Loc.t -> 'a -> glob_constr
+type prim_token_uid = string
 
-type cases_pattern_status = bool (* true = use prim token in patterns *)
+type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr
+type 'a prim_token_uninterpreter = any_glob_constr -> 'a option
 
-type 'a prim_token_uninterpreter =
-    glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
+type 'a prim_token_interpretation =
+  'a prim_token_interpreter * 'a prim_token_uninterpreter
 
-type internal_prim_token_interpreter =
-    ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr)
+module InnerPrimToken = struct
 
-let prim_token_interpreter_tab =
-  (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
+  type interpreter =
+    | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr)
+    | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr)
+    | StringInterp of (?loc:Loc.t -> string -> glob_constr)
 
-let add_prim_token_interpreter sc interp =
-  try
-    let cont = Hashtbl.find prim_token_interpreter_tab sc in
-    Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
-  with Not_found ->
-    let cont = (fun ?loc _p -> raise Not_found) in
-    Hashtbl.add prim_token_interpreter_tab sc (interp cont)
+  let interp_eq f f' = match f,f' with
+    | RawNumInterp f, RawNumInterp f' -> f == f'
+    | BigNumInterp f, BigNumInterp f' -> f == f'
+    | StringInterp f, StringInterp f' -> f == f'
+    | _ -> false
 
-let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
-  declare_scope sc;
-  add_prim_token_interpreter sc interp;
-  List.iter (fun pat ->
-      prim_token_key_table := KeyMap.add
-        (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table)
-    patl
+  let ofNumeral n s =
+    if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
 
-let mkNumeral n =
-  if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
-  else Numeral (Bigint.to_string (Bigint.neg n), false)
+  let do_interp ?loc interp primtok =
+    match primtok, interp with
+    | Numeral (n,s), RawNumInterp interp -> interp ?loc (n,s)
+    | Numeral (n,s), BigNumInterp interp -> interp ?loc (ofNumeral n s)
+    | String s, StringInterp interp -> interp ?loc s
+    | _ -> raise Not_found
 
-let ofNumeral n s =
-  if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+  type uninterpreter =
+    | RawNumUninterp of (any_glob_constr -> rawnum option)
+    | BigNumUninterp of (any_glob_constr -> Bigint.bigint option)
+    | StringUninterp of (any_glob_constr -> string option)
 
-let mkString = function
-| None -> None
-| Some s -> if Unicode.is_utf8 s then Some (String s) else None
+  let uninterp_eq f f' = match f,f' with
+    | RawNumUninterp f, RawNumUninterp f' -> f == f'
+    | BigNumUninterp f, BigNumUninterp f' -> f == f'
+    | StringUninterp f, StringUninterp f' -> f == f'
+    | _ -> false
 
-let delay dir int ?loc x = (dir, (fun () -> int ?loc x))
+  let mkNumeral n =
+    if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
+    else Numeral (Bigint.to_string (Bigint.neg n), false)
 
-type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+  let mkString = function
+    | None -> None
+    | Some s -> if Unicode.is_utf8 s then Some (String s) else None
+
+  let do_uninterp uninterp g = match uninterp with
+    | RawNumUninterp u -> Option.map (fun (n,s) -> Numeral (n,s)) (u g)
+    | BigNumUninterp u -> Option.map mkNumeral (u g)
+    | StringUninterp u -> mkString (u g)
+
+end
+
+(* The following two tables of (un)interpreters will *not* be synchronized.
+   But their indexes will be checked to be unique *)
+let prim_token_interpreters =
+  (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t)
+
+let prim_token_uninterpreters =
+  (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t)
+
+(* Table from scope_name to backtrack-able informations about interpreters
+   (in particular interpreter unique id). *)
+let prim_token_interp_infos =
+  ref (String.Map.empty : (required_module * prim_token_uid) String.Map.t)
+
+(* Table from global_reference to backtrack-able informations about
+   prim_token uninterpretation (in particular uninterpreter unique id). *)
+let prim_token_uninterp_infos =
+  ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t)
+
+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 allow_overwrite uid (interp, uninterp) =
+  hashtbl_check_and_set
+    allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq;
+  hashtbl_check_and_set
+    allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
+
+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 ?(allow_overwrite=false) uid (interp, uninterp) =
+  register_gen_interpretation allow_overwrite uid
+    (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp)
+
+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_local : bool; (** Is this interpretation local? *)
+  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 : GlobRef.t list; (** Entry points during uninterpretation *)
+  pt_in_match : bool (** Is this prim token legal in match patterns ? *)
+}
+
+let cache_prim_token_interpretation (_,infos) =
+  let sc = infos.pt_scope in
+  let uid = infos.pt_uid in
+  declare_scope sc;
+  prim_token_interp_infos :=
+    String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos;
+  List.iter (fun r -> prim_token_uninterp_infos :=
+                        Refmap.add r (sc,uid,infos.pt_in_match)
+                          !prim_token_uninterp_infos)
+            infos.pt_refs
+
+let subst_prim_token_interpretation (subs,infos) =
+  { infos with
+    pt_refs = List.map (subst_global_reference subs) infos.pt_refs }
+
+let classify_prim_token_interpretation infos =
+    if infos.pt_local then Dispose else Substitute infos
+
+let inPrimTokenInterp : prim_token_infos -> obj =
+  declare_object {(default_object "PRIM-TOKEN-INTERP") with
+     open_function  = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o);
+     cache_function = cache_prim_token_interpretation;
+     subst_function = subst_prim_token_interpretation;
+     classify_function = classify_prim_token_interpretation}
+
+let enable_prim_token_interpretation infos =
+  Lib.add_anonymous_leaf (inPrimTokenInterp infos)
+
+(** Compatibility.
+    Avoid the next two functions, they will now store unnecessary
+    objects in the library segment. Instead, combine
+    [register_*_interpretation] and [enable_prim_token_interpretation]
+    (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 ?(local=false) sc dir interp (patl,uninterp,b) =
+  let uid = fresh_string_of sc in
+  register_bignumeral_interpretation uid (interp,uninterp);
+  enable_prim_token_interpretation
+    { pt_local = local;
+      pt_scope = 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 ?(local=false) sc dir interp (patl,uninterp,b) =
+  let uid = fresh_string_of sc in
+  register_string_interpretation uid (interp,uninterp);
+  enable_prim_token_interpretation
+    { pt_local = local;
+      pt_scope = sc;
+      pt_uid = uid;
+      pt_required = dir;
+      pt_refs = List.map_filter glob_prim_constr_key patl;
+      pt_in_match = b }
 
-let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) =
-  declare_prim_token_interpreter sc
-    (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s)
-                            | p -> cont ?loc p)
-    (patl, (fun r -> match uninterp r with
-                     | None -> None
-                     | Some (n,s) -> Some (Numeral (n,s))), inpat)
-
-let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
-  let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in
-  declare_prim_token_interpreter sc
-    (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s)
-                            | p -> cont ?loc p)
-    (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
-
-let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
-  declare_prim_token_interpreter sc
-    (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p)
-    (patl, (fun r -> mkString (uninterp r)), inpat)
 
 let check_required_module ?loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
-    user_err ?loc ~hdr:"prim_token_interpreter"
-    (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
+    match d with
+    | [] -> user_err ?loc ~hdr:"prim_token_interpreter"
+       (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.")
+    | _ -> user_err ?loc ~hdr:"prim_token_interpreter"
+       (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
@@ -476,9 +586,10 @@ let find_prim_token check_allowed ?loc p sc =
     pat, df
   with Not_found ->
   (* Try for a primitive numerical notation *)
-  let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc ?loc p in
+  let (spdir,uid) = String.Map.find sc !prim_token_interp_infos in
   check_required_module ?loc sc spdir;
-  let pat = interp () in
+  let interp = Hashtbl.find prim_token_interpreters uid in
+  let pat = InnerPrimToken.do_interp ?loc interp p in
   check_allowed pat;
   pat, ((dirpath (fst spdir),DirPath.empty),"")
 
@@ -649,43 +760,34 @@ let entry_has_ident = function
      try String.Map.find s !entry_has_ident_map <= n with Not_found -> false
 
 let uninterp_prim_token c =
-  try
-    let (sc,numpr,_) =
-      KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in
-    match numpr (AnyGlobConstr c) with
-      | None -> raise Notation_ops.No_match
-      | Some n -> (sc,n)
-  with Not_found -> raise Notation_ops.No_match
-
-let uninterp_prim_token_ind_pattern ind args =
-  let ref = IndRef ind in
-  try
-    let k = RefKey (canonical_gr ref) in
-    let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in
-    if not b then raise Notation_ops.No_match;
-    let args' = List.map
-      (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
-    let ref = DAst.make @@ GRef (ref,None) in
-    match numpr (AnyGlobConstr (DAst.make @@ GApp (ref,args'))) with
-      | None -> raise Notation_ops.No_match
-      | Some n -> (sc,n)
-  with Not_found -> raise Notation_ops.No_match
+  match glob_prim_constr_key c with
+  | None -> raise Notation_ops.No_match
+  | Some r ->
+     try
+       let (sc,uid,_) = Refmap.find r !prim_token_uninterp_infos in
+       let uninterp = Hashtbl.find prim_token_uninterpreters uid in
+       match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
+       | None -> raise Notation_ops.No_match
+       | Some n -> (sc,n)
+     with Not_found -> raise Notation_ops.No_match
 
 let uninterp_prim_token_cases_pattern c =
-  try
-    let k = cases_pattern_key c in
-    let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in
-    if not b then raise Notation_ops.No_match;
-    let na,c = glob_constr_of_closed_cases_pattern c in
-    match numpr (AnyGlobConstr c) with
-      | None -> raise Notation_ops.No_match
-      | Some n -> (na,sc,n)
-  with Not_found -> raise Notation_ops.No_match
+  match glob_constr_of_closed_cases_pattern c with
+  | exception Not_found -> raise Notation_ops.No_match
+  | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n)
 
 let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
-    try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true
-    with Not_found -> false in
+    try
+      let uid = snd (String.Map.find scope !prim_token_interp_infos) in
+      let interp = Hashtbl.find prim_token_interpreters uid in
+      let open InnerPrimToken in
+      match n, interp with
+      | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+      | String _, StringInterp _ -> true
+      | _ -> false
+    with Not_found -> false
+  in
   let scopes = make_current_scopes local_scopes in
   Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
@@ -1206,16 +1308,19 @@ let pr_visibility prglob = function
 let freeze _ =
  (!scope_map, !scope_stack, !arguments_scope,
   !delimiters_map, !notations_key_table, !scope_class_map,
+  !prim_token_interp_infos, !prim_token_uninterp_infos,
   !entry_coercion_map, !entry_has_global_map,
   !entry_has_ident_map)
 
-let unfreeze (scm,scs,asc,dlm,fkm,clsc,coe,globs,ids) =
+let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) =
   scope_map := scm;
   scope_stack := scs;
   delimiters_map := dlm;
   arguments_scope := asc;
   notations_key_table := fkm;
   scope_class_map := clsc;
+  prim_token_interp_infos := ptii;
+  prim_token_uninterp_infos := ptui;
   entry_coercion_map := coe;
   entry_has_global_map := globs;
   entry_has_ident_map := ids
@@ -1224,7 +1329,9 @@ let init () =
   init_scope_map ();
   delimiters_map := String.Map.empty;
   notations_key_table := KeyMap.empty;
-  scope_class_map := initial_scope_class_map
+  scope_class_map := initial_scope_class_map;
+  prim_token_interp_infos := String.Map.empty;
+  prim_token_uninterp_infos := Refmap.empty
 
 let _ =
   Summary.declare_summary "symbols"
diff --git a/interp/notation.mli b/interp/notation.mli
index c921606484..e5478eff48 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Bigint
 open Names
 open Libnames
 open Constrexpr
@@ -75,24 +74,62 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
 
 type notation_location = (DirPath.t * DirPath.t) * string
 type required_module = full_path * string list
-type cases_pattern_status = bool (** true = use prim token in patterns *)
+type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
 
-type 'a prim_token_interpreter =
-    ?loc:Loc.t -> 'a -> glob_constr
+(** The unique id string below will be used to refer to a particular
+    registered interpreter/uninterpreter of numeral or string notation.
+    Using the same uid for different (un)interpreters will fail.
+    If at most one interpretation of prim token is used per scope,
+    then the scope name could be used as unique id. *)
 
-type 'a prim_token_uninterpreter =
-    glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
+type prim_token_uid = string
 
-type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr
+type 'a prim_token_uninterpreter = any_glob_constr -> 'a option
+
+type 'a prim_token_interpretation =
+  'a prim_token_interpreter * 'a prim_token_uninterpreter
+
+val register_rawnumeral_interpretation :
+  ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit
+
+val register_bignumeral_interpretation :
+  ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit
+
+val register_string_interpretation :
+  ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
+
+type prim_token_infos = {
+  pt_local : bool; (** Is this interpretation local? *)
+  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 : GlobRef.t list; (** Entry points during uninterpretation *)
+  pt_in_match : bool (** Is this prim token legal in match patterns ? *)
+}
+
+(** Note: most of the time, the [pt_refs] field above will contain
+    inductive constructors (e.g. O and S for nat). But it could also be
+    injection functions such as IZR for reals. *)
+
+(** Activate a prim token interpretation whose unique id and functions
+    have already been registered. *)
 
-val declare_rawnumeral_interpreter : scope_name -> required_module ->
-  rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit
+val enable_prim_token_interpretation : prim_token_infos -> unit
 
-val declare_numeral_interpreter : scope_name -> required_module ->
-  bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit
+(** Compatibility.
+    Avoid the next two functions, they will now store unnecessary
+    objects in the library segment. Instead, combine
+    [register_*_interpretation] and [enable_prim_token_interpretation]
+    (the latter inside a [Mltop.declare_cache_obj]).
+*)
 
-val declare_string_interpreter : scope_name -> required_module ->
-  string prim_token_interpreter -> string prim_token_uninterpreter -> unit
+val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module ->
+  Bigint.bigint prim_token_interpreter ->
+  glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit
+val declare_string_interpreter : ?local:bool -> scope_name -> required_module ->
+  string prim_token_interpreter ->
+  glob_constr list * string prim_token_uninterpreter * bool -> unit
 
 (** Return the [term]/[cases_pattern] bound to a primitive token in a
    given scope context*)
@@ -110,8 +147,6 @@ val uninterp_prim_token :
   'a glob_constr_g -> scope_name * prim_token
 val uninterp_prim_token_cases_pattern :
   'a cases_pattern_g -> Name.t * scope_name * prim_token
-val uninterp_prim_token_ind_pattern :
- inductive -> cases_pattern list -> scope_name * prim_token
 
 val availability_of_prim_token :
   prim_token -> scope_name -> subscopes -> delimiters option option
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index dbbdbfa396..d779951180 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -52,8 +52,11 @@ let () =
 
 (* Rewriting orientation *)
 
-let _ = Metasyntax.add_token_obj "<-"
-let _ = Metasyntax.add_token_obj "->"
+let _ =
+  Mltop.declare_cache_obj
+    (fun () -> Metasyntax.add_token_obj "<-";
+               Metasyntax.add_token_obj "->")
+    "ltac_plugin"
 
 let pr_orient _prc _prlc _prt = function
   | true -> Pp.mt ()
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 0bb9ccb1d8..1f2c722b34 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -144,7 +144,7 @@ let add ~deprecation kn b t =
   mactab := KNmap.add kn entry !mactab
 
 let replace kn path t =
-  let (path, _, _) = KerName.repr path in
+  let path = KerName.modpath path in
   let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
   mactab := KNmap.modify kn entry !mactab
 
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 47a59ba631..5e36fbeb81 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -83,8 +83,18 @@ let make_ascii_string n =
 
 let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r)
 
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
 let _ =
-  Notation.declare_string_interpreter "char_scope"
-    (ascii_path,ascii_module)
-    interp_ascii_string
-    ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
+  let sc = "char_scope" in
+  register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = sc;
+      pt_uid = sc;
+      pt_required = (ascii_path,ascii_module);
+      pt_refs = [static_glob_Ascii];
+      pt_in_match = true }
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
new file mode 100644
index 0000000000..ec14df3baa
--- /dev/null
+++ b/plugins/syntax/g_numeral.ml4
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*         *   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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+DECLARE PLUGIN "numeral_notation_plugin"
+
+open Numeral
+open Pp
+open Names
+open Vernacinterp
+open Ltac_plugin
+open Stdarg
+open Pcoq.Prim
+
+let pr_numnot_option _ _ _ = function
+  | Nop -> mt ()
+  | Warning n -> str "(warning after " ++ str n ++ str ")"
+  | Abstract n -> str "(abstract after " ++ str n ++ str ")"
+
+ARGUMENT EXTEND numnotoption
+  PRINTED BY pr_numnot_option
+| [ ] -> [ Nop ]
+| [ "(" "warning" "after" bigint(waft) ")" ] -> [ Warning waft ]
+| [ "(" "abstract" "after" bigint(n) ")" ] -> [ Abstract n ]
+END
+
+VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
+  | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+      ident(sc) numnotoption(o) ] ->
+    [ vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o ]
+END
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index f10f98e23b..d3ffe936a9 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -96,10 +96,19 @@ let uninterp_int31 (AnyGlobConstr i) =
   with Non_closed ->
     None
 
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
 (* Actually declares the interpreter for int31 *)
-let _ = Notation.declare_numeral_interpreter int31_scope
-  (int31_path, int31_module)
-  interp_int31
-  ([DAst.make (GRef (int31_construct, None))],
-   uninterp_int31,
-   true)
+
+let _ =
+  register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = int31_scope;
+      pt_uid = int31_scope;
+      pt_required = (int31_path,int31_module);
+      pt_refs = [int31_construct];
+      pt_in_match = true }
diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml
deleted file mode 100644
index 0e202be47f..0000000000
--- a/plugins/syntax/n_syntax.ml
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(*         *   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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Pp
-open CErrors
-open Names
-open Bigint
-open Positive_syntax_plugin.Positive_syntax
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "n_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-(**********************************************************************)
-(* Parsing N via scopes                                               *)
-(**********************************************************************)
-
-open Globnames
-open Glob_term
-
-let binnums = ["Coq";"Numbers";"BinNums"]
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-(* TODO: temporary hack *)
-let make_kn dir id = Globnames.encode_mind dir id
-
-let n_kn = make_kn (make_dir binnums) (Id.of_string "N")
-let glob_n = IndRef (n_kn,0)
-let path_of_N0 = ((n_kn,0),1)
-let path_of_Npos = ((n_kn,0),2)
-let glob_N0 = ConstructRef path_of_N0
-let glob_Npos = ConstructRef path_of_Npos
-
-let n_path = make_path binnums "N"
-
-let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@
-  if not (Bigint.equal n zero) then
-    GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
-  else
-    GRef(glob_N0, None)
-
-let error_negative ?loc =
-  user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".")
-
-let n_of_int ?loc n =
-  if is_pos_or_zero n then n_of_binnat ?loc true n
-  else error_negative ?loc
-
-(**********************************************************************)
-(* Printing N via scopes                                              *)
-(**********************************************************************)
-
-let bignat_of_n n = DAst.with_val (function
-  | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a
-  | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero
-  | _ -> raise Non_closed_number
-  ) n
-
-let uninterp_n (AnyGlobConstr p) =
-  try Some (bignat_of_n p)
-  with Non_closed_number -> None
-
-(************************************************************************)
-(* Declaring interpreters and uninterpreters for N *)
-
-let _ = Notation.declare_numeral_interpreter "N_scope"
-  (n_path,binnums)
-  n_of_int
-  ([DAst.make @@ GRef (glob_N0, None);
-    DAst.make @@ GRef (glob_Npos, None)],
-  uninterp_n,
-  true)
diff --git a/plugins/syntax/n_syntax_plugin.mlpack b/plugins/syntax/n_syntax_plugin.mlpack
deleted file mode 100644
index 4c56645f07..0000000000
--- a/plugins/syntax/n_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-N_syntax
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
deleted file mode 100644
index e158e0b516..0000000000
--- a/plugins/syntax/nat_syntax.ml
+++ /dev/null
@@ -1,85 +0,0 @@
-(************************************************************************)
-(*         *   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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "nat_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-(* This file defines the printer for natural numbers in [nat] *)
-
-(*i*)
-open Pp
-open CErrors
-open Names
-open Glob_term
-open Bigint
-open Coqlib
-(*i*)
-
-(**********************************************************************)
-(* Parsing via scopes *)
-(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
-
-let threshold = of_int 5000
-
-let warn_large_nat =
-  CWarnings.create ~name:"large-nat" ~category:"numbers"
-    (fun () -> strbrk "Stack overflow or segmentation fault happens when " ++
-                 strbrk "working with large numbers in nat (observed threshold " ++
-                 strbrk "may vary from 5000 to 70000 depending on your system " ++
-                 strbrk "limits and on the command executed).")
-
-let nat_of_int ?loc n =
-  if is_pos_or_zero n then begin
-      if less_than threshold n then warn_large_nat ();
-      let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in
-      let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in
-      let rec mk_nat acc n =
-	if n <> zero then
-	  mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
-	else
-	  acc
-      in
-      mk_nat ref_O n
-    end
-  else
-      user_err ?loc ~hdr:"nat_of_int"
-       (str "Cannot interpret a negative number as a number of type nat")
-
-(************************************************************************)
-(* Printing via scopes *)
-
-exception Non_closed_number
-
-let rec int_of_nat x = DAst.with_val (function
-  | GApp (r, [a]) ->
-    begin match DAst.get r with
-    | GRef (s,_) when GlobRef.equal s glob_S -> add_1 (int_of_nat a)
-    | _ -> raise Non_closed_number
-    end
-  | GRef (z,_) when GlobRef.equal z glob_O -> zero
-  | _ -> raise Non_closed_number
-  ) x
-
-let uninterp_nat (AnyGlobConstr p) =
-  try
-    Some (int_of_nat p)
-  with
-    Non_closed_number -> None
-
-(************************************************************************)
-(* Declare the primitive parsers and printers *)
-
-let _ =
-  Notation.declare_numeral_interpreter "nat_scope"
-    (nat_path,datatypes_module_name)
-    nat_of_int
-    ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true)
diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack
deleted file mode 100644
index 39bdd62f47..0000000000
--- a/plugins/syntax/nat_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Nat_syntax
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
new file mode 100644
index 0000000000..fee93593d0
--- /dev/null
+++ b/plugins/syntax/numeral.ml
@@ -0,0 +1,478 @@
+(************************************************************************)
+(*         *   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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Libnames
+open Globnames
+open Constrexpr
+open Constrexpr_ops
+open Constr
+
+(** * Numeral notation *)
+
+(** Reduction
+
+    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
+    applied.
+
+    At least [c] is known to be evar-free, since it comes from
+    our own ad-hoc [constr_of_glob] or from conversions such
+    as [coqint_of_rawnum].
+*)
+
+let eval_constr env sigma (c : Constr.t) =
+  let c = EConstr.of_constr c in
+  let sigma,t = Typing.type_of env sigma c in
+  let c' = Vnorm.cbv_vm env sigma c t in
+  EConstr.Unsafe.to_constr c'
+
+(* For testing with "compute" instead of "vm_compute" :
+let eval_constr env sigma (c : Constr.t) =
+  let c = EConstr.of_constr c in
+  let c' = Tacred.compute env sigma c in
+  EConstr.Unsafe.to_constr c'
+*)
+
+let eval_constr_app env sigma c1 c2 =
+  eval_constr env sigma (mkApp (c1,[| c2 |]))
+
+exception NotANumber
+
+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_qualid ty ++
+      strbrk " (threshold may vary depending" ++
+      strbrk " on your system limits and on the command executed).")
+
+let warn_abstract_large_num =
+  CWarnings.create ~name:"abstract-large-number" ~category:"numbers"
+    (fun (ty,f) ->
+      strbrk "To avoid stack overflow, large numbers in " ++
+      pr_qualid ty ++ strbrk " are interpreted as applications of " ++
+      Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
+
+let warn_abstract_large_num_no_op =
+  CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
+    (fun f ->
+      strbrk "The 'abstract after' directive has no effect when " ++
+      strbrk "the parsing function (" ++
+      Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
+      strbrk "option type.")
+
+(** Comparing two raw numbers (base 10, big-endian, non-negative).
+    A bit nasty, but not critical: only used to decide when a
+    number is considered as large (see warnings above). *)
+
+exception Comp of int
+
+let rec rawnum_compare s s' =
+ let l = String.length s and l' = String.length s' in
+ if l < l' then - rawnum_compare s' s
+ else
+   let d = l-l' in
+   try
+     for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
+     for i = d to l-1 do
+       let c = Pervasives.compare s.[i] s'.[i-d] in
+       if c != 0 then raise (Comp c)
+     done;
+     0
+   with Comp c -> c
+
+(***********************************************************************)
+
+(** ** Conversion between Coq [Decimal.int] and internal raw string *)
+
+type int_ty =
+  { uint : Names.inductive;
+    int : Names.inductive }
+
+(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *)
+
+let digit_of_char c =
+  assert ('0' <= c && c <= '9');
+  Char.code c - Char.code '0' + 2
+
+let char_of_digit n =
+  assert (2<=n && n<=11);
+  Char.chr (n-2 + Char.code '0')
+
+let coquint_of_rawnum uint str =
+  let nil = mkConstruct (uint,1) in
+  let rec do_chars s i acc =
+    if i < 0 then acc
+    else
+      let dg = mkConstruct (uint, digit_of_char s.[i]) in
+      do_chars s (i-1) (mkApp(dg,[|acc|]))
+  in
+  do_chars str (String.length str - 1) nil
+
+let coqint_of_rawnum inds (str,sign) =
+  let uint = coquint_of_rawnum inds.uint str in
+  mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|])
+
+let rawnum_of_coquint c =
+  let rec of_uint_loop c buf =
+    match Constr.kind c with
+    | Construct ((_,1), _) (* Nil *) -> ()
+    | App (c, [|a|]) ->
+       (match Constr.kind c with
+        | Construct ((_,n), _) (* D0 to D9 *) ->
+           let () = Buffer.add_char buf (char_of_digit n) in
+           of_uint_loop a buf
+        | _ -> raise NotANumber)
+    | _ -> raise NotANumber
+  in
+  let buf = Buffer.create 64 in
+  let () = of_uint_loop c buf in
+  if Int.equal (Buffer.length buf) 0 then
+    (* To avoid ambiguities between Nil and (D0 Nil), we choose
+       to not display Nil alone as "0" *)
+    raise NotANumber
+  else Buffer.contents buf
+
+let rawnum_of_coqint c =
+  match Constr.kind c with
+  | App (c,[|c'|]) ->
+     (match Constr.kind c with
+      | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true)
+      | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false)
+      | _ -> raise NotANumber)
+  | _ -> raise NotANumber
+
+
+(***********************************************************************)
+
+(** ** Conversion between Coq [Z] and internal bigint *)
+
+type z_pos_ty =
+  { z_ty : Names.inductive;
+    pos_ty : Names.inductive }
+
+(** First, [positive] from/to bigint *)
+
+let rec pos_of_bigint posty n =
+  match Bigint.div2_with_rest n with
+  | (q, false) ->
+      let c = mkConstruct (posty, 2) in (* xO *)
+      mkApp (c, [| pos_of_bigint posty q |])
+  | (q, true) when not (Bigint.equal q Bigint.zero) ->
+      let c = mkConstruct (posty, 1) in (* xI *)
+      mkApp (c, [| pos_of_bigint posty q |])
+  | (q, true) ->
+      mkConstruct (posty, 3) (* xH *)
+
+let rec bigint_of_pos c = match Constr.kind c with
+  | Construct ((_, 3), _) -> (* xH *) Bigint.one
+  | App (c, [| d |]) ->
+      begin match Constr.kind c with
+      | Construct ((_, n), _) ->
+          begin match n with
+          | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d))
+          | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d)
+          | n -> assert false (* no other constructor of type positive *)
+          end
+      | x -> raise NotANumber
+      end
+  | x -> raise NotANumber
+
+(** Now, [Z] from/to bigint *)
+
+let z_of_bigint { z_ty; pos_ty } n =
+  if Bigint.equal n Bigint.zero then
+    mkConstruct (z_ty, 1) (* Z0 *)
+  else
+    let (s, n) =
+      if Bigint.is_pos_or_zero n then (2, n) (* Zpos *)
+      else (3, Bigint.neg n) (* Zneg *)
+    in
+    let c = mkConstruct (z_ty, s) in
+    mkApp (c, [| pos_of_bigint pos_ty n |])
+
+let bigint_of_z z = match Constr.kind z with
+  | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero
+  | App (c, [| d |]) ->
+      begin match Constr.kind c with
+      | Construct ((_, n), _) ->
+          begin match n with
+          | 2 -> (* Zpos *) bigint_of_pos d
+          | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d)
+          | n -> assert false (* no other constructor of type Z *)
+          end
+      | _ -> raise NotANumber
+      end
+  | _ -> raise NotANumber
+
+(** The uninterp function below work at the level of [glob_constr]
+    which is too low for us here. So here's a crude conversion back
+    to [constr] for the subset that concerns us. *)
+
+let rec constr_of_glob env sigma g = match DAst.get g with
+  | Glob_term.GRef (ConstructRef c, _) ->
+      let sigma,c = Evd.fresh_constructor_instance env sigma c in
+      sigma,mkConstructU c
+  | Glob_term.GApp (gc, gcl) ->
+      let sigma,c = constr_of_glob env sigma gc in
+      let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
+      sigma,mkApp (c, Array.of_list cl)
+  | _ ->
+      raise NotANumber
+
+let rec glob_of_constr ?loc c = match Constr.kind c with
+  | App (c, ca) ->
+      let c = glob_of_constr ?loc c in
+      let cel = List.map (glob_of_constr ?loc) (Array.to_list ca) in
+      DAst.make ?loc (Glob_term.GApp (c, cel))
+  | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
+  | 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))
+  | _ -> let (sigma, env) = Pfedit.get_current_context () in
+         CErrors.user_err ?loc
+           (strbrk "Unexpected term " ++
+              Printer.pr_constr_env env sigma c ++
+              strbrk " while parsing a numeral notation.")
+
+let no_such_number ?loc ty =
+  CErrors.user_err ?loc
+   (str "Cannot interpret this number as a value of type " ++
+    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 -> let (sigma, env) = Pfedit.get_current_context () in
+         CErrors.user_err ?loc
+          (strbrk "Unexpected non-option term " ++
+             Printer.pr_constr_env env sigma c ++
+             strbrk " while parsing a numeral notation.")
+
+let uninterp_option c =
+  match Constr.kind c with
+  | App (_Some, [| _; x |]) -> x
+  | _ -> raise NotANumber
+
+let big2raw n =
+  if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
+  else (Bigint.to_string (Bigint.neg n), false)
+
+let raw2big (n,s) =
+  if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+
+type target_kind =
+  | Int of int_ty (* Coq.Init.Decimal.int + uint *)
+  | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
+  | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
+
+type option_kind = Option | Direct
+type conversion_kind = target_kind * option_kind
+
+type numnot_option =
+  | Nop
+  | Warning of raw_natural_number
+  | Abstract of raw_natural_number
+
+type numeral_notation_obj =
+  { to_kind : conversion_kind;
+    to_ty : GlobRef.t;
+    of_kind : conversion_kind;
+    of_ty : GlobRef.t;
+    num_ty : Libnames.qualid; (* for warnings / error messages *)
+    warning : numnot_option }
+
+let interp o ?loc n =
+  begin match o.warning with
+  | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
+     warn_large_num o.num_ty
+  | _ -> ()
+  end;
+  let c = match fst o.to_kind with
+    | Int int_ty -> coqint_of_rawnum int_ty n
+    | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n)
+    | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty
+    | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n)
+  in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in
+  let to_ty = EConstr.Unsafe.to_constr to_ty in
+  match o.warning, snd o.to_kind with
+  | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 ->
+     warn_abstract_large_num (o.num_ty,o.to_ty);
+     glob_of_constr ?loc (mkApp (to_ty,[|c|]))
+  | _ ->
+     let res = eval_constr_app env sigma to_ty c in
+     match snd o.to_kind with
+     | Direct -> glob_of_constr ?loc res
+     | Option -> interp_option o.num_ty ?loc res
+
+let uninterp o (Glob_term.AnyGlobConstr n) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in
+  let of_ty = EConstr.Unsafe.to_constr of_ty in
+  try
+    let sigma,n = constr_of_glob env sigma n in
+    let c = eval_constr_app env sigma of_ty n in
+    let c = if snd o.of_kind == Direct then c else uninterp_option c in
+    match fst o.of_kind with
+    | Int _ -> Some (rawnum_of_coqint c)
+    | UInt _ -> Some (rawnum_of_coquint c, true)
+    | Z _ -> Some (big2raw (bigint_of_z c))
+  with
+  | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
+  | NotANumber -> None (* all other functions except big2raw *)
+
+(* Here we only register the interp and uninterp functions
+   for a particular Numeral Notation (determined by a unique
+   string). The actual activation of the notation will be done
+   later (cf. Notation.enable_prim_token_interpretation).
+   This registration of interp/uninterp must be added in the
+   libstack, otherwise this won't work through a Require. *)
+
+let load_numeral_notation _ (_, (uid,opts)) =
+  Notation.register_rawnumeral_interpretation
+    ~allow_overwrite:true uid (interp opts, uninterp opts)
+
+let cache_numeral_notation x = load_numeral_notation 1 x
+
+(* TODO: substitution ?
+   TODO: uid pas stable par substitution dans opts
+ *)
+
+let inNumeralNotation : string * numeral_notation_obj -> Libobject.obj =
+  Libobject.declare_object {
+    (Libobject.default_object "NUMERAL NOTATION") with
+    Libobject.cache_function = cache_numeral_notation;
+    Libobject.load_function = load_numeral_notation }
+
+let get_constructors ind =
+  let mib,oib = Global.lookup_inductive ind in
+  let mc = oib.Declarations.mind_consnames in
+  Array.to_list
+    (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
+
+let q_z = qualid_of_string "Coq.Numbers.BinNums.Z"
+let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive"
+let q_int = qualid_of_string "Coq.Init.Decimal.int"
+let q_uint = qualid_of_string "Coq.Init.Decimal.uint"
+let q_option = qualid_of_string "Coq.Init.Datatypes.option"
+
+let unsafe_locate_ind q =
+  match Nametab.locate q with
+  | IndRef i -> i
+  | _ -> raise Not_found
+
+let locate_ind q =
+  try unsafe_locate_ind q
+  with Not_found -> Nametab.error_global_not_found q
+
+let locate_z () =
+  try
+    Some { z_ty = unsafe_locate_ind q_z;
+           pos_ty = unsafe_locate_ind q_positive }
+  with Not_found -> None
+
+let locate_int () =
+  { uint = locate_ind q_uint;
+    int = locate_ind q_int }
+
+let has_type f ty =
+  let (sigma, env) = Pfedit.get_current_context () 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_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_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 local ty f g scope opts =
+  let int_ty = locate_int () in
+  let z_pos_ty = locate_z () in
+  let tyc = Smartlocate.global_inductive_with_alias ty in
+  let to_ty = Smartlocate.global_with_alias f in
+  let of_ty = Smartlocate.global_with_alias g in
+  let cty = mkRefC ty in
+  let app x y = mkAppC (x,[y]) in
+  let cref q = mkRefC q in
+  let arrow x y =
+    mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
+  in
+  let cZ = cref q_z in
+  let cint = cref q_int in
+  let cuint = cref q_uint in
+  let coption = cref q_option in
+  let opt r = app coption r in
+  let constructors = get_constructors tyc in
+  (* Check the type of f *)
+  let to_kind =
+    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
+    else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option
+    else
+      match z_pos_ty with
+      | Some z_pos_ty ->
+         if has_type f (arrow cZ cty) then Z z_pos_ty, Direct
+         else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option
+         else type_error_to f ty false
+      | None -> type_error_to f ty true
+  in
+  (* Check the type of g *)
+  let of_kind =
+    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
+    else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option
+    else
+      match z_pos_ty with
+      | Some z_pos_ty ->
+         if has_type g (arrow cty cZ) then Z z_pos_ty, Direct
+         else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option
+         else type_error_of g ty false
+      | None -> type_error_of g ty true
+  in
+  let o = { to_kind; to_ty; of_kind; of_ty;
+            num_ty = ty;
+            warning = opts }
+  in
+  (match opts, to_kind with
+   | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty
+   | _ -> ());
+  (* TODO: un hash suffit-il ? *)
+  let uid = Marshal.to_string o [] in
+  let i = Notation.(
+       { pt_local = local;
+         pt_scope = scope;
+         pt_uid = uid;
+         pt_required = Nametab.path_of_global (IndRef tyc),[];
+         pt_refs = constructors;
+         pt_in_match = true })
+  in
+  Lib.add_anonymous_leaf (inNumeralNotation (uid,o));
+  Notation.enable_prim_token_interpretation i
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
new file mode 100644
index 0000000000..83ede6f48f
--- /dev/null
+++ b/plugins/syntax/numeral.mli
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*         *   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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Libnames
+open Constrexpr
+open Vernacexpr
+
+(** * Numeral notation *)
+
+type numnot_option =
+  | Nop
+  | Warning of raw_natural_number
+  | Abstract of raw_natural_number
+
+val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack
new file mode 100644
index 0000000000..f4d9cae3ff
--- /dev/null
+++ b/plugins/syntax/numeral_notation_plugin.mlpack
@@ -0,0 +1,2 @@
+Numeral
+G_numeral
diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml
deleted file mode 100644
index 0c82e47445..0000000000
--- a/plugins/syntax/positive_syntax.ml
+++ /dev/null
@@ -1,101 +0,0 @@
-(************************************************************************)
-(*         *   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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Pp
-open CErrors
-open Util
-open Names
-open Bigint
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "positive_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-exception Non_closed_number
-
-(**********************************************************************)
-(* Parsing positive via scopes                                        *)
-(**********************************************************************)
-
-open Globnames
-open Glob_term
-
-let binnums = ["Coq";"Numbers";"BinNums"]
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-let positive_path = make_path binnums "positive"
-
-(* TODO: temporary hack *)
-let make_kn dir id = Globnames.encode_mind dir id
-
-let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
-let glob_positive = IndRef (positive_kn,0)
-let path_of_xI = ((positive_kn,0),1)
-let path_of_xO = ((positive_kn,0),2)
-let path_of_xH = ((positive_kn,0),3)
-let glob_xI = ConstructRef path_of_xI
-let glob_xO = ConstructRef path_of_xO
-let glob_xH = ConstructRef path_of_xH
-
-let pos_of_bignat ?loc x =
-  let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in
-  let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in
-  let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in
-  let rec pos_of x =
-    match div2_with_rest x with
-      | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q])
-      | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q])
-      | (q,true) -> ref_xH
-  in
-  pos_of x
-
-let error_non_positive ?loc =
-  user_err ?loc ~hdr:"interp_positive"
-   (str "Only strictly positive numbers in type \"positive\".")
-
-let interp_positive ?loc n =
-  if is_strictly_pos n then pos_of_bignat ?loc n
-  else error_non_positive ?loc
-
-(**********************************************************************)
-(* Printing positive via scopes                                       *)
-(**********************************************************************)
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-let rec bignat_of_pos x = DAst.with_val (function
-  | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
-  | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (a, _)                when GlobRef.equal a glob_xH -> Bigint.one
-  | _ -> raise Non_closed_number
-  ) x
-
-let uninterp_positive (AnyGlobConstr p) =
-  try
-    Some (bignat_of_pos p)
-  with Non_closed_number ->
-    None
-
-(************************************************************************)
-(* Declaring interpreters and uninterpreters for positive *)
-(************************************************************************)
-
-let _ = Notation.declare_numeral_interpreter "positive_scope"
-  (positive_path,binnums)
-  interp_positive
-  ([DAst.make @@ GRef (glob_xI, None);
-    DAst.make @@ GRef (glob_xO, None);
-    DAst.make @@ GRef (glob_xH, None)],
-   uninterp_positive,
-   true)
diff --git a/plugins/syntax/positive_syntax_plugin.mlpack b/plugins/syntax/positive_syntax_plugin.mlpack
deleted file mode 100644
index ac8f3c425c..0000000000
--- a/plugins/syntax/positive_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Positive_syntax
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 94aa143350..04946c158b 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -131,9 +131,19 @@ let uninterp_r (AnyGlobConstr p) =
   with Non_closed_number ->
     None
 
-let _ = Notation.declare_numeral_interpreter "R_scope"
-  (r_path,["Coq";"Reals";"Rdefinitions"])
-  r_of_int
-  ([DAst.make @@ GRef (glob_IZR, None)],
-    uninterp_r,
-    false)
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
+let r_scope = "R_scope"
+
+let _ =
+  register_bignumeral_interpretation r_scope (r_of_int,uninterp_r);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = r_scope;
+      pt_uid = r_scope;
+      pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
+      pt_refs = [glob_IZR];
+      pt_in_match = false }
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index c22869f4d6..640bcfde91 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -64,10 +64,18 @@ let uninterp_string (AnyGlobConstr r) =
   with
    Non_closed_string -> None
 
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
 let _ =
-  Notation.declare_string_interpreter "string_scope"
-    (string_path,["Coq";"Strings";"String"])
-    interp_string
-    ([DAst.make @@ GRef (static_glob_String,None);
-      DAst.make @@ GRef (static_glob_EmptyString,None)],
-     uninterp_string, true)
+  let sc = "string_scope" in
+  register_string_interpretation sc (interp_string,uninterp_string);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = sc;
+      pt_uid = sc;
+      pt_required = (string_path,["Coq";"Strings";"String"]);
+      pt_refs = [static_glob_String; static_glob_EmptyString];
+      pt_in_match = true }
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
deleted file mode 100644
index 2534162e36..0000000000
--- a/plugins/syntax/z_syntax.ml
+++ /dev/null
@@ -1,78 +0,0 @@
-(************************************************************************)
-(*         *   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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open Bigint
-open Positive_syntax_plugin.Positive_syntax
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "z_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-(**********************************************************************)
-(* Parsing Z via scopes                                               *)
-(**********************************************************************)
-
-open Globnames
-open Glob_term
-
-let binnums = ["Coq";"Numbers";"BinNums"]
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-(* TODO: temporary hack *)
-let make_kn dir id = Globnames.encode_mind dir id
-
-let z_path = make_path binnums "Z"
-let z_kn = make_kn (make_dir binnums) (Id.of_string "Z")
-let glob_z = IndRef (z_kn,0)
-let path_of_ZERO = ((z_kn,0),1)
-let path_of_POS = ((z_kn,0),2)
-let path_of_NEG = ((z_kn,0),3)
-let glob_ZERO = ConstructRef path_of_ZERO
-let glob_POS = ConstructRef path_of_POS
-let glob_NEG = ConstructRef path_of_NEG
-
-let z_of_int ?loc n =
-  if not (Bigint.equal n zero) then
-    let sgn, n =
-      if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
-  else
-    DAst.make ?loc @@ GRef(glob_ZERO, None)
-
-(**********************************************************************)
-(* Printing Z via scopes                                              *)
-(**********************************************************************)
-
-let bigint_of_z z = DAst.with_val (function
-  | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a
-  | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero
-  | _ -> raise Non_closed_number
-  ) z
-
-let uninterp_z (AnyGlobConstr p) =
-  try
-    Some (bigint_of_z p)
-  with Non_closed_number -> None
-
-(************************************************************************)
-(* Declaring interpreters and uninterpreters for Z *)
-
-let _ = Notation.declare_numeral_interpreter "Z_scope"
-  (z_path,binnums)
-  z_of_int
-  ([DAst.make @@ GRef (glob_ZERO, None);
-    DAst.make @@ GRef (glob_POS, None);
-    DAst.make @@ GRef (glob_NEG, None)],
-  uninterp_z,
-  true)
diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack
deleted file mode 100644
index 411260c04c..0000000000
--- a/plugins/syntax/z_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Z_syntax
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 117d6523a8..f8cedfff6e 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -23,7 +23,9 @@ Module Export Datatypes.
 
 Set Implicit Arguments.
 Notation nat := Coq.Init.Datatypes.nat.
+Notation O := Coq.Init.Datatypes.O.
 Notation S := Coq.Init.Datatypes.S.
+Notation two := (S (S O)).
 
 Record prod (A B : Type) := pair { fst : A ; snd : B }.
 
@@ -159,7 +161,7 @@ End Adjointify.
            (n : nat) {A : Type@{i}} {B : Type@{j}}
            (f : A -> B) (C : B -> Type@{k}) : Type@{l}
     := match n with
-         | 0 => Unit@{l}
+         | O => Unit@{l}
          | S n => (forall (g : forall a, C (f a)),
                      ExtensionAlong@{i j k l l} f C g) *
                   forall (h k : forall b, C b),
@@ -220,12 +222,12 @@ Section ORecursion.
   Definition O_indpaths {P Q : Type} {Q_inO : In O Q}
              (g h : O P -> Q) (p : g o to O P == h o to O P)
   : g == h
-  := (fst (snd (extendable_to_O O 2) g h) p).1.
+  := (fst (snd (extendable_to_O O two) g h) p).1.
 
   Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q}
              (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P)
   : O_indpaths g h p (to O P x) = p x
-  := (fst (snd (extendable_to_O O 2) g h) p).2 x.
+  := (fst (snd (extendable_to_O O two) g h) p).2 x.
 
 End ORecursion.
 
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index c3e0da1117..fd2380a070 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -17,7 +17,10 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope.
 Module Export Datatypes.
   Set Implicit Arguments.
   Notation nat := Coq.Init.Datatypes.nat.
+  Notation O := Coq.Init.Datatypes.O.
   Notation S := Coq.Init.Datatypes.S.
+  Notation one := (S O).
+  Notation two := (S one).
   Record prod (A B : Type) := pair { fst : A ; snd : B }.
   Notation "x * y" := (prod x y) : type_scope.
   Delimit Scope nat_scope with nat.
@@ -109,7 +112,7 @@ Fixpoint ExtendableAlong@{i j k l}
          (n : nat) {A : Type@{i}} {B : Type@{j}}
          (f : A -> B) (C : B -> Type@{k}) : Type@{l}
   := match n with
-     | 0 => Unit@{l}
+     | O => Unit@{l}
      | S n => (forall (g : forall a, C (f a)),
                   ExtensionAlong@{i j k l l} f C g) *
               forall (h k : forall b, C b),
@@ -160,17 +163,17 @@ Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses).
     Definition O_rec {P Q : Type} {Q_inO : In O Q}
                (f : P -> Q)
       : O P -> Q
-      := (fst (extendable_to_O O 1%nat) f).1.
+      := (fst (extendable_to_O O one) f).1.
 
     Definition O_rec_beta {P Q : Type} {Q_inO : In O Q}
                (f : P -> Q) (x : P)
       : O_rec f (to O P x) = f x
-      := (fst (extendable_to_O O 1%nat) f).2 x.
+      := (fst (extendable_to_O O one) f).2 x.
 
     Definition O_indpaths {P Q : Type} {Q_inO : In O Q}
                (g h : O P -> Q) (p : g o to O P == h o to O P)
       : g == h
-      := (fst (snd (extendable_to_O O 2) g h) p).1.
+      := (fst (snd (extendable_to_O O two) g h) p).1.
 
   End ORecursion.
 
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index 4ad53bc629..13c47edc8f 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -19,6 +19,7 @@ Inductive sum (A B : Type) : Type :=
   | inl : A -> sum A B
   | inr : B -> sum A B.
 Notation nat := Coq.Init.Datatypes.nat.
+Notation O := Coq.Init.Datatypes.O.
 Notation S := Coq.Init.Datatypes.S.
 Notation "x + y" := (sum x y) : type_scope.
 
@@ -449,7 +450,7 @@ Section Extensions.
            (n : nat) {A : Type@{i}} {B : Type@{j}}
            (f : A -> B) (C : B -> Type@{k}) : Type@{l}
     := match n with
-         | 0 => Unit@{l}
+         | O => Unit@{l}
          | S n => (forall (g : forall a, C (f a)),
                      ExtensionAlong@{i j k l l} f C g) *
                   forall (h k : forall b, C b),
diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v
new file mode 100644
index 0000000000..07986b0df3
--- /dev/null
+++ b/test-suite/interactive/PrimNotation.v
@@ -0,0 +1,64 @@
+(* Until recently, the Notation.declare_numeral_notation wasn't synchronized
+   w.r.t. backtracking. This should be ok now.
+   This test is pretty artificial (we must declare Z_scope for this to work).
+*)
+
+Delimit Scope Z_scope with Z.
+Open Scope Z_scope.
+Check let v := 0 in v : nat.
+(* let v := 0 in v : nat : nat *)
+Require BinInt.
+Check let v := 0 in v : BinNums.Z.
+(* let v := 0 in v : BinNums.Z : BinNums.Z *)
+Back 2.
+Check let v := 0 in v : nat.
+(* Expected answer: let v := 0 in v : nat : nat *)
+(* Used to fail with:
+Error: Cannot interpret in Z_scope without requiring first module BinNums.
+*)
+
+Local Set Universe Polymorphism.
+Delimit Scope punit_scope with punit.
+Delimit Scope pcunit_scope with pcunit.
+Delimit Scope int_scope with int.
+Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope.
+Module A.
+  NonCumulative Inductive punit@{u} : Type@{u} := ptt.
+  Cumulative Inductive pcunit@{u} : Type@{u} := pctt.
+  Definition to_punit : Decimal.int -> option punit
+    := fun v => match v with 0%int => Some ptt | _ => None end.
+  Definition to_pcunit : Decimal.int -> option pcunit
+    := fun v => match v with 0%int => Some pctt | _ => None end.
+  Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+  Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0.
+  Numeral Notation punit to_punit of_punit : punit_scope.
+  Check let v := 0%punit in v : punit.
+  Back 2.
+  Numeral Notation pcunit to_pcunit of_pcunit : punit_scope.
+  Check let v := 0%punit in v : pcunit.
+End A.
+Reset A.
+Local Unset Universe Polymorphism.
+Module A.
+  Inductive punit : Set := ptt.
+  Definition to_punit : Decimal.int -> option punit
+    := fun v => match v with 0%int => Some ptt | _ => None end.
+  Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+  Numeral Notation punit to_punit of_punit : punit_scope.
+  Check let v := 0%punit in v : punit.
+End A.
+Local Set Universe Polymorphism.
+Inductive punit@{u} : Type@{u} := ptt.
+Definition to_punit : Decimal.int -> option punit
+  := fun v => match v with 0%int => Some ptt | _ => None end.
+Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+Numeral Notation punit to_punit of_punit : punit_scope.
+Check let v := 0%punit in v : punit.
+Back 6. (* check backtracking of registering universe polymorphic constants *)
+Local Unset Universe Polymorphism.
+Inductive punit : Set := ptt.
+Definition to_punit : Decimal.int -> option punit
+  := fun v => match v with 0%int => Some ptt | _ => None end.
+Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+Numeral Notation punit to_punit of_punit : punit_scope.
+Check let v := 0%punit in v : punit.
diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v
new file mode 100644
index 0000000000..e2045900d5
--- /dev/null
+++ b/test-suite/success/Compat88.v
@@ -0,0 +1,18 @@
+(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(** Check that various syntax usage is available without importing
+    relevant files. *)
+Require Coq.Strings.Ascii Coq.Strings.String.
+Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
+Require Coq.Reals.Rdefinitions.
+Require Coq.Numbers.Cyclic.Int31.Cyclic31.
+
+Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *)
+
+Check String.String "a" String.EmptyString.
+Check String.eqb "a" "a".
+Check Nat.eqb 1 1.
+Check BinNat.N.eqb 1 1.
+Check BinInt.Z.eqb 1 1.
+Check BinPos.Pos.eqb 1 1.
+Check Rdefinitions.Rplus 1 1.
+Check Int31.iszero 1.
diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
new file mode 100644
index 0000000000..47ef381270
--- /dev/null
+++ b/test-suite/success/NumeralNotations.v
@@ -0,0 +1,302 @@
+(* 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 NonCumulative 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 pto_punit_all (v : Decimal.uint) : punit := ptt.
+  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.
+  Numeral Notation punit to_punit of_punit : pto.
+  Numeral Notation punit pto_punit of_punit : ppo.
+  Numeral Notation punit to_punit pof_punit : ptp.
+  Numeral Notation punit pto_punit pof_punit : ppp.
+  Numeral Notation unit to_unit of_unit : uto.
+  Delimit Scope pto with pto.
+  Delimit Scope ppo with ppo.
+  Delimit Scope ptp with ptp.
+  Delimit Scope ppp with ppp.
+  Delimit Scope uto with uto.
+  Check let v := 0%pto in v : punit.
+  Check let v := 0%ppo in v : punit.
+  Check let v := 0%ptp in v : punit.
+  Check let v := 0%ppp in v : punit.
+  Check let v := 0%uto in v : unit.
+  Fail Check 1%uto.
+  Fail Check (-1)%uto.
+  Numeral Notation unit pto_unit of_unit : upo.
+  Numeral Notation unit to_unit pof_unit : utp.
+  Numeral Notation unit pto_unit pof_unit : upp.
+  Delimit Scope upo with upo.
+  Delimit Scope utp with utp.
+  Delimit Scope upp with upp.
+  Check let v := 0%upo in v : unit.
+  Check let v := 0%utp in v : unit.
+  Check let v := 0%upp in v : unit.
+
+  Polymorphic Definition pto_punits := pto_punit_all@{Set}.
+  Polymorphic Definition pof_punits := pof_punit@{Set}.
+  Numeral Notation punit pto_punits pof_punits : ppps (abstract after 1).
+  Delimit Scope ppps with ppps.
+  Universe u.
+  Constraint Set < u.
+  Check let v := 0%ppps in v : punit@{u}. (* Check that universes are refreshed *)
+  Fail Check let v := 1%ppps in v : punit@{u}. (* Note that universes are not refreshed here *)
+End Test4.
+
+Module Test5.
+  Check S. (* At one point gave Error: Anomaly "Uncaught exception Pretype_errors.PretypeError(_, _, _)." Please report at http://coq.inria.fr/bugs/. *)
+End Test5.
+
+Module Test6.
+  (* Check that numeral notations on enormous terms don't take forever to print/parse *)
+  (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *)
+  Fixpoint ack (n m : nat) : nat :=
+    match n with
+    | O => S m
+    | S p => let fix ackn (m : nat) :=
+                 match m with
+                 | O => ack p 1
+                 | S q => ack p (ackn q)
+                 end
+             in ackn m
+    end.
+
+  Timeout 1 Check (S (ack 4 4)). (* should be instantaneous *)
+
+  Local Set Primitive Projections.
+  Record > wnat := wrap { unwrap :> nat }.
+  Definition to_uint (x : wnat) : Decimal.uint := Nat.to_uint x.
+  Definition of_uint (x : Decimal.uint) : wnat := Nat.of_uint x.
+  Module Export Scopes.
+    Delimit Scope wnat_scope with wnat.
+  End Scopes.
+  Module Export Notations.
+    Export Scopes.
+    Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000).
+  End Notations.
+  Check let v := 0%wnat in v : wnat.
+  Check wrap O.
+  Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *)
+End Test6.
+
+Module Test6_2.
+  Import Test6.Scopes.
+  Check Test6.wrap 0.
+  Import Test6.Notations.
+  Check let v := 0%wnat in v : Test6.wnat.
+End Test6_2.
+
+Module Test7.
+  Local Set Primitive Projections.
+  Record wuint := wrap { unwrap : Decimal.uint }.
+  Delimit Scope wuint_scope with wuint.
+  Numeral Notation wuint wrap unwrap : wuint_scope.
+  Check let v := 0%wuint in v : wuint.
+  Check let v := 1%wuint in v : wuint.
+End Test7.
+
+Module Test8.
+  Local Set Primitive Projections.
+  Record wuint := wrap { unwrap : Decimal.uint }.
+  Delimit Scope wuint8_scope with wuint8.
+  Delimit Scope wuint8'_scope with wuint8'.
+  Section with_var.
+    Context (dummy : unit).
+    Definition wrap' := let __ := dummy in wrap.
+    Definition unwrap' := let __ := dummy in unwrap.
+    Numeral Notation wuint wrap' unwrap' : wuint8_scope.
+    Check let v := 0%wuint8 in v : wuint.
+  End with_var.
+  Check let v := 0%wuint8 in v : nat.
+  Fail Check let v := 0%wuint8 in v : wuint.
+  Compute wrap (Nat.to_uint 0).
+
+  Notation wrap'' := wrap.
+  Notation unwrap'' := unwrap.
+  Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope.
+  Check let v := 0%wuint8' in v : wuint.
+End Test8.
+
+Module Test9.
+  Delimit Scope wuint9_scope with wuint9.
+  Delimit Scope wuint9'_scope with wuint9'.
+  Section with_let.
+    Local Set Primitive Projections.
+    Record wuint := wrap { unwrap : Decimal.uint }.
+    Let wrap' := wrap.
+    Let unwrap' := unwrap.
+    Local Notation wrap'' := wrap.
+    Local Notation unwrap'' := unwrap.
+    Numeral Notation wuint wrap' unwrap' : wuint9_scope.
+    Check let v := 0%wuint9 in v : wuint.
+    Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope.
+    Check let v := 0%wuint9' in v : wuint.
+  End with_let.
+  Check let v := 0%wuint9 in v : nat.
+  Fail Check let v := 0%wuint9 in v : wuint.
+End Test9.
+
+Module Test10.
+  (* Test that it is only a warning to add abstract after to an optional parsing function *)
+  Definition to_uint (v : unit) := Nat.to_uint 0.
+  Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end.
+  Definition of_any_uint (v : Decimal.uint) := tt.
+  Delimit Scope unit_scope with unit.
+  Delimit Scope unit2_scope with unit2.
+  Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1).
+  Local Set Warnings Append "+abstract-large-number-no-op".
+  (* Check that there is actually a warning here *)
+  Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1).
+  (* Check that there is no warning here *)
+  Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1).
+End Test10.
+
+Module Test11.
+  (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
+  Inductive unit11 := tt11.
+  Delimit Scope unit11_scope with unit11.
+  Goal True.
+    evar (to_uint : unit11 -> Decimal.uint).
+    evar (of_uint : Decimal.uint -> unit11).
+    Fail Numeral Notation unit11 of_uint to_uint : uint11_scope.
+    exact I.
+    Unshelve.
+    all: solve [ constructor ].
+  Qed.
+End Test11.
+
+Module Test12.
+  (* Test for numeral notations on context variables *)
+  Delimit Scope test12_scope with test12.
+  Section test12.
+    Context (to_uint : unit -> Decimal.uint) (of_uint : Decimal.uint -> unit).
+
+    Numeral Notation unit of_uint to_uint : test12_scope.
+    Check let v := 1%test12 in v : unit.
+  End test12.
+End Test12.
+
+Module Test13.
+  (* Test for numeral notations on notations which do not denote references *)
+  Delimit Scope test13_scope with test13.
+  Delimit Scope test13'_scope with test13'.
+  Delimit Scope test13''_scope with test13''.
+  Definition to_uint (x y : unit) : Decimal.uint := Nat.to_uint O.
+  Definition of_uint (x : Decimal.uint) : unit := tt.
+  Definition to_uint_good := to_uint tt.
+  Notation to_uint' := (to_uint tt).
+  Notation to_uint'' := (to_uint _).
+  Numeral Notation unit of_uint to_uint_good : test13_scope.
+  Check let v := 0%test13 in v : unit.
+  Fail Numeral Notation unit of_uint to_uint' : test13'_scope.
+  Fail Check let v := 0%test13' in v : unit.
+  Fail Numeral Notation unit of_uint to_uint'' : test13''_scope.
+  Fail Check let v := 0%test13'' in v : unit.
+End Test13.
+
+Module Test14.
+  (* Test that numeral notations follow [Import], not [Require], and
+     also test that [Local Numeral Notation]s do not escape modules
+     nor sections. *)
+  Delimit Scope test14_scope with test14.
+  Delimit Scope test14'_scope with test14'.
+  Delimit Scope test14''_scope with test14''.
+  Delimit Scope test14'''_scope with test14'''.
+  Module Inner.
+    Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O.
+    Definition of_uint (x : Decimal.uint) : unit := tt.
+    Local Numeral Notation unit of_uint to_uint : test14_scope.
+    Global Numeral Notation unit of_uint to_uint : test14'_scope.
+    Check let v := 0%test14 in v : unit.
+    Check let v := 0%test14' in v : unit.
+  End Inner.
+  Fail Check let v := 0%test14 in v : unit.
+  Fail Check let v := 0%test14' in v : unit.
+  Import Inner.
+  Fail Check let v := 0%test14 in v : unit.
+  Check let v := 0%test14' in v : unit.
+  Section InnerSection.
+    Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O.
+    Definition of_uint (x : Decimal.uint) : unit := tt.
+    Local Numeral Notation unit of_uint to_uint : test14''_scope.
+    Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope.
+    Check let v := 0%test14'' in v : unit.
+    Fail Check let v := 0%test14''' in v : unit.
+  End InnerSection.
+  Fail Check let v := 0%test14'' in v : unit.
+  Fail Check let v := 0%test14''' in v : unit.
+End Test14.
+
+Module Test15.
+  (** Test module include *)
+  Delimit Scope test15_scope with test15.
+  Module Inner.
+    Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O.
+    Definition of_uint (x : Decimal.uint) : unit := tt.
+    Numeral Notation unit of_uint to_uint : test15_scope.
+    Check let v := 0%test15 in v : unit.
+  End Inner.
+  Module Inner2.
+    Include Inner.
+    Check let v := 0%test15 in v : unit.
+  End Inner2.
+  Import Inner Inner2.
+  Check let v := 0%test15 in v : unit.
+End Test15.
+
+Module Test16.
+  (** Test functors *)
+  Delimit Scope test16_scope with test16.
+  Module Type A.
+    Axiom T : Set.
+    Axiom t : T.
+  End A.
+  Module F (a : A).
+    Inductive Foo := foo (_ : a.T).
+    Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O.
+    Definition of_uint (x : Decimal.uint) : Foo := foo a.t.
+    Global Numeral Notation Foo of_uint to_uint : test16_scope.
+    Check let v := 0%test16 in v : Foo.
+  End F.
+  Module a <: A.
+    Definition T : Set := unit.
+    Definition t : T := tt.
+  End a.
+  Module Import f := F a.
+  (** Ideally this should work, but it should definitely not anomaly *)
+  Fail Check let v := 0%test16 in v : Foo.
+End Test16.
diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
index 4142af05d2..578425bfb5 100644
--- a/theories/Compat/Coq88.v
+++ b/theories/Compat/Coq88.v
@@ -9,3 +9,17 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
+(** In Coq 8.9, prim token notations follow [Import] rather than
+    [Require].  So we make all of the relevant notations accessible in
+    compatibility mode. *)
+Require Coq.Strings.Ascii Coq.Strings.String.
+Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
+Require Coq.Reals.Rdefinitions.
+Require Coq.Numbers.Cyclic.Int31.Int31.
+Declare ML Module "string_syntax_plugin".
+Declare ML Module "ascii_syntax_plugin".
+Declare ML Module "r_syntax_plugin".
+Declare ML Module "int31_syntax_plugin".
+Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope.
+Numeral Notation BinNums.positive BinPosDef.Pos.of_int BinPosDef.Pos.to_int : positive_scope.
+Numeral Notation BinNums.N BinNatDef.N.of_int BinNatDef.N.to_int : N_scope.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 05b741f0ac..1e6843d511 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -12,7 +12,6 @@ Set Implicit Arguments.
 
 Require Import Notations.
 Require Import Logic.
-Declare ML Module "nat_syntax_plugin".
 
 (********************************************************************)
 (** * Datatypes with zero and one element *)
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 57163b1b07..1ff00ec11c 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -42,10 +42,10 @@ Notation zero := (D0 Nil).
 
 Inductive int := Pos (d:uint) | Neg (d:uint).
 
-Delimit Scope uint_scope with uint.
-Bind Scope uint_scope with uint.
-Delimit Scope int_scope with int.
-Bind Scope int_scope with int.
+Delimit Scope dec_uint_scope with uint.
+Bind Scope dec_uint_scope with uint.
+Delimit Scope dec_int_scope with int.
+Bind Scope dec_int_scope with int.
 
 (** This representation favors simplicity over canonicity.
     For normalizing numbers, we need to remove head zero digits,
@@ -161,3 +161,9 @@ with succ_double d :=
   end.
 
 End Little.
+
+(** Pseudo-conversion functions used when declaring
+    Numeral Notations on [uint] and [int]. *)
+
+Definition uint_of_uint (i:uint) := i.
+Definition int_of_int (i:int) := i.
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index ad1bc717c4..eb4ba0e5e6 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -24,6 +24,10 @@ Definition t := nat.
 
 (** ** Constants *)
 
+Local Notation "0" := O.
+Local Notation "1" := (S O).
+Local Notation "2" := (S (S O)).
+
 Definition zero := 0.
 Definition one := 1.
 Definition two := 2.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index d5322d0945..65e5e76a22 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -31,6 +31,7 @@ Require Import Logic.
 Require Coq.Init.Nat.
 
 Open Scope nat_scope.
+Local Notation "0" := O.
 
 Definition eq_S := f_equal S.
 Definition f_equal_nat := f_equal (A:=nat).
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 802f18c0f2..6d98bcb34a 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -19,9 +19,24 @@ Require Export Peano.
 Require Export Coq.Init.Wf.
 Require Export Coq.Init.Tactics.
 Require Export Coq.Init.Tauto.
-(* Initially available plugins
-   (+ nat_syntax_plugin loaded in Datatypes) *)
+(* Some initially available plugins. See also:
+   - ltac_plugin (in Notations)
+   - tauto_plugin (in Tauto).
+*)
 Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
+Declare ML Module "numeral_notation_plugin".
+
+(* Parsing / printing of decimal numbers *)
+Arguments Nat.of_uint d%dec_uint_scope.
+Arguments Nat.of_int d%dec_int_scope.
+Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint
+  : dec_uint_scope.
+Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
+  : dec_int_scope.
+
+(* Parsing / printing of [nat] numbers *)
+Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000).
+
 (* Default substrings not considered by queries like SearchAbout *)
 Add Search Blacklist "_subproof" "_subterm" "Private_".
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 5d3ec5abc7..bd27f94abd 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N.
 
 (** Exportation of notations *)
 
+Numeral Notation N N.of_uint N.to_uint : N_scope.
+
 Infix "+" := N.add : N_scope.
 Infix "-" := N.sub : N_scope.
 Infix "*" := N.mul : N_scope.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 5de75537cb..be12fffaaf 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -13,6 +13,10 @@ Require Import BinPos.
 
 Local Open Scope N_scope.
 
+Local Notation "0" := N0.
+Local Notation "1" := (Npos 1).
+Local Notation "2" := (Npos 2).
+
 (**********************************************************************)
 (** * Binary natural numbers, definitions of operations *)
 (**********************************************************************)
@@ -398,4 +402,9 @@ Definition to_uint n :=
 
 Definition to_int n := Decimal.Pos (to_uint n).
 
+Numeral Notation N of_uint to_uint : N_scope.
+
 End N.
+
+(** Re-export the notation for those who just [Import NatIntDef] *)
+Numeral Notation N N.of_uint N.to_uint : N_scope.
diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
new file mode 100644
index 0000000000..c7e3999691
--- /dev/null
+++ b/theories/Numbers/AltBinNotations.v
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*         *   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          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * Alternative Binary Numeral Notations *)
+
+(** Faster but less safe parsers and printers of [positive], [N], [Z]. *)
+
+(** 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. 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.
+
+(** [positive] *)
+
+Definition pos_of_z z :=
+  match z with
+    | Zpos p => Some p
+    | _ => None
+  end.
+
+Definition pos_to_z p := Zpos p.
+
+Numeral Notation positive pos_of_z pos_to_z : positive_scope.
+
+(** [N] *)
+
+Definition n_of_z z :=
+  match z with
+    | Z0 => Some N0
+    | Zpos p => Some (Npos p)
+    | Zneg _ => None
+  end.
+
+Definition n_to_z n :=
+ match n with
+   | N0 => Z0
+   | Npos p => Zpos p
+ end.
+
+Numeral Notation N n_of_z n_to_z : N_scope.
+
+(** [Z] *)
+
+Definition z_of_z (z:Z) := z.
+
+Numeral Notation Z z_of_z z_of_z : Z_scope.
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index d5eb4f2681..3ba9d1f5ed 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -12,15 +12,11 @@
 
 Set Implicit Arguments.
 
-Declare ML Module "positive_syntax_plugin".
-Declare ML Module "n_syntax_plugin".
-Declare ML Module "z_syntax_plugin".
-
 (** [positive] is a datatype representing the strictly positive integers
    in a binary way. Starting from 1 (represented by [xH]), one can
    add a new least significant digit via [xO] (digit 0) or [xI] (digit 1).
-   Numbers in [positive] can also be denoted using a decimal notation;
-   e.g. [6%positive] abbreviates [xO (xI xH)] *)
+   Numbers in [positive] will also be denoted using a decimal notation;
+   e.g. [6%positive] will abbreviate [xO (xI xH)] *)
 
 Inductive positive : Set :=
   | xI : positive -> positive
@@ -34,8 +30,8 @@ Arguments xI _%positive.
 
 (** [N] is a datatype representing natural numbers in a binary way,
     by extending the [positive] datatype with a zero.
-    Numbers in [N] can also be denoted using a decimal notation;
-    e.g. [6%N] abbreviates [Npos (xO (xI xH))] *)
+    Numbers in [N] will also be denoted using a decimal notation;
+    e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *)
 
 Inductive N : Set :=
   | N0 : N
@@ -49,8 +45,8 @@ Arguments Npos _%positive.
     An integer is either zero or a strictly positive number
     (coded as a [positive]) or a strictly negative number
     (whose opposite is stored as a [positive] value).
-    Numbers in [Z] can also be denoted using a decimal notation;
-    e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *)
+    Numbers in [Z] will also be denoted using a decimal notation;
+    e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *)
 
 Inductive Z : Set :=
   | Z0 : Z
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index bd4f0279d4..ec480bb1eb 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -23,8 +23,6 @@ Require Import Zpow_facts.
 Require Import CyclicAxioms.
 Require Import ROmega.
 
-Declare ML Module "int31_syntax_plugin".
-
 Local Open Scope nat_scope.
 Local Open Scope int31_scope.
 
@@ -128,7 +126,7 @@ Section Basics.
 
  Lemma nshiftl_S_tail :
   forall n x, nshiftl x (S n) = nshiftl (shiftl x) n.
- Proof. 
+ Proof.
  intros n; elim n; simpl; intros; now f_equal.
  Qed.
 
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 9f8da831d8..39af62c32f 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -15,6 +15,8 @@ Require Import Wf_nat.
 Require Export ZArith.
 Require Export DoubleType.
 
+Declare ML Module "int31_syntax_plugin".
+
 (** * 31-bit integers *)
 
 (** This file contains basic definitions of a 31-bit integer
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 000d895e10..dcaae1606d 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1871,6 +1871,8 @@ Bind Scope positive_scope with Pos.t positive.
 
 (** Exportation of notations *)
 
+Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope.
+
 Infix "+" := Pos.add : positive_scope.
 Infix "-" := Pos.sub : positive_scope.
 Infix "*" := Pos.mul : positive_scope.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 070314746a..7f30733559 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -26,6 +26,8 @@ Require Export BinNums.
     for the number 6 (which is 110 in binary notation).
 *)
 
+Local Notation "1" := xH.
+
 Notation "p ~ 1" := (xI p)
  (at level 7, left associativity, format "p '~' '1'") : positive_scope.
 Notation "p ~ 0" := (xO p)
@@ -325,14 +327,14 @@ Definition sqrtrem_step (f g:positive->positive) p :=
     let r' := g (f r) in
     if s' <=? r' then (s~1, sub_mask r' s')
     else (s~0, IsPos r')
-  | (s,_)  => (s~0, sub_mask (g (f 1)) 4)
+  | (s,_)  => (s~0, sub_mask (g (f 1)) 1~0~0)
  end.
 
 Fixpoint sqrtrem p : positive * mask :=
  match p with
   | 1 => (1,IsNul)
-  | 2 => (1,IsPos 1)
-  | 3 => (1,IsPos 2)
+  | 1~0 => (1,IsPos 1)
+  | 1~1 => (1,IsPos 1~0)
   | p~0~0 => sqrtrem_step xO xO (sqrtrem p)
   | p~0~1 => sqrtrem_step xO xI (sqrtrem p)
   | p~1~0 => sqrtrem_step xI xO (sqrtrem p)
@@ -614,4 +616,9 @@ Definition to_uint p := Decimal.rev (to_little_uint p).
 
 Definition to_int n := Decimal.Pos (to_uint n).
 
+Numeral Notation positive of_int to_uint : positive_scope.
+
 End Pos.
+
+(** Re-export the notation for those who just [Import BinPosDef] *)
+Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index cf7397b57e..a11d491a8b 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z.
 
 (** Re-export Notations *)
 
+Numeral Notation Z Z.of_int Z.to_int : Z_scope.
+
 Infix "+" := Z.add : Z_scope.
 Notation "- x" := (Z.opp x) : Z_scope.
 Infix "-" := Z.sub : Z_scope.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index db4de0b90c..8cb62622db 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -14,6 +14,10 @@ Require Import BinPos BinNat.
 
 Local Open Scope Z_scope.
 
+Local Notation "0" := Z0.
+Local Notation "1" := (Zpos 1).
+Local Notation "2" := (Zpos 2).
+
 (***********************************************************)
 (** * Binary Integers, Definitions of Operations *)
 (***********************************************************)
@@ -53,7 +57,7 @@ Definition succ_double x :=
 
 Definition pred_double x :=
   match x with
-    | 0 => -1
+    | 0 => neg 1
     | neg p => neg p~1
     | pos p => pos (Pos.pred_double p)
   end.
@@ -104,7 +108,7 @@ Definition succ x := x + 1.
 
 (** ** Predecessor *)
 
-Definition pred x := x + -1.
+Definition pred x := x + neg 1.
 
 (** ** Subtraction *)
 
@@ -171,7 +175,7 @@ Definition sgn z :=
   match z with
     | 0 => 0
     | pos p => 1
-    | neg p => -1
+    | neg p => neg 1
   end.
 
 (** Boolean equality and comparisons *)
@@ -635,4 +639,9 @@ Definition lxor a b :=
    | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
  end.
 
+Numeral Notation Z of_int to_int : Z_scope.
+
 End Z.
+
+(** Re-export the notation for those who just [Import BinIntDef] *)
+Numeral Notation Z Z.of_int Z.to_int : Z_scope.