prim notations backtrackable, their declarations now in two parts (API change)

 The first part (e.g. register_bignumeral_interpretation) deals only with
 the interp/uninterp closures. It should typically be done as a side
 effect during a syntax plugin loading. No prim notation are active yet
 after this phase.

 The second part (enable_prim_token_interpretation) activates the prim
 notation. It is now correctly talking to Summary and to the LibStack.
 To avoid "phantom" objects in libstack after a mere Require, this
 second part should be done inside a Mltop.declare_cache_obj

 The link between the two parts is a prim_token_uid (a string), which
 should be unique for each primitive notation. When this primitive
 notation is specific to a scope, the scope_name could be used as uid.

 Btw, the list of "patterns" for detecting when an uninterpreter should
 be considered is now restricted to a list of global_reference
 (inductive constructors, or injection functions such as IZR).
 The earlier API was accepting a glob_constr list, but was actually
 only working well for global_reference.

 A minimal compatibility is provided (declare_numeral_interpreter),
 but is discouraged, since it is known to store uncessary objects
 in the libstack.

11 files changed, 365 insertions, 145 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index ebb734cb08..f60ddcf909 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,63 +301,167 @@ 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 '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
+
+module InnerPrimToken = struct
 
-type cases_pattern_status = bool (* true = use prim token in patterns *)
+  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)
 
-type 'a prim_token_uninterpreter =
-    glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
+  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 ofNumeral n s =
+    if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+
+  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
+
+  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 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
 
-type internal_prim_token_interpreter =
-  | ForNumeral of rawnum prim_token_interpreter
-  | ForString of string prim_token_interpreter
+  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 prim_token_interpreter_tab =
-  (Hashtbl.create 7 :
-     (scope_name, required_module * internal_prim_token_interpreter) Hashtbl.t)
+  let mkString = function
+    | None -> None
+    | Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
-let add_prim_token_interpreter sc (dir,interp) =
-  Hashtbl.replace prim_token_interpreter_tab sc (dir,interp)
+  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)
 
-let declare_prim_token_interpreter sc (dir,interp) (patl,uninterp,b) =
+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 uid f h eq =
+  match Hashtbl.find h uid with
+   | exception Not_found -> Hashtbl.add h uid f
+   | g when eq f g -> ()
+   | _ ->
+      user_err ~hdr:"prim_token_interpreter"
+       (str "Unique identifier " ++ str uid ++
+        str " already used to register a numeral or string (un)interpreter.")
+
+let register_gen_interpretation uid (interp, uninterp) =
+  hashtbl_check_and_set
+    uid interp prim_token_interpreters InnerPrimToken.interp_eq;
+  hashtbl_check_and_set
+    uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
+
+let register_rawnumeral_interpretation uid (interp, uninterp) =
+  register_gen_interpretation uid
+    (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp)
+
+let register_bignumeral_interpretation uid (interp, uninterp) =
+  register_gen_interpretation uid
+    (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp)
+
+let register_string_interpretation uid (interp, uninterp) =
+  register_gen_interpretation uid
+    (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp)
+
+type prim_token_infos = {
+  pt_scope : scope_name; (** Concerned scope *)
+  pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
+  pt_required : required_module; (** Module that should be loaded first *)
+  pt_refs : global_reference list; (** Entry points during uninterpretation *)
+  pt_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;
-  add_prim_token_interpreter sc (dir,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 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 ofNumeral n s =
-  if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
-
-let mkString = function
-| None -> None
-| Some s -> if Unicode.is_utf8 s then Some (String s) else None
-
-let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) =
-  declare_prim_token_interpreter sc
-    (dir, ForNumeral interp)
-    (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) =
-  declare_prim_token_interpreter sc
-    (dir, ForNumeral (fun ?loc (n,s) -> interp ?loc (ofNumeral n s)))
-    (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
-
-let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
-  declare_prim_token_interpreter sc
-    (dir, ForString interp)
-    (patl, (fun r -> mkString (uninterp r)), inpat)
+  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 inPrimTokenInterp : prim_token_infos -> obj =
+  declare_object {(default_object "PRIM-TOKEN-INTERP") with
+     cache_function = cache_prim_token_interpretation;
+     load_function  = (fun _ -> cache_prim_token_interpretation);
+     subst_function = subst_prim_token_interpretation;
+     classify_function = (fun o -> Substitute o)}
+
+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 declare_numeral_interpreter sc dir interp (patl,uninterp,b) =
+  register_bignumeral_interpretation sc (interp,uninterp);
+  enable_prim_token_interpretation
+    { pt_scope = sc;
+      pt_uid = sc;
+      pt_required = dir;
+      pt_refs = List.map_filter glob_prim_constr_key patl;
+      pt_in_match = b }
+let declare_string_interpreter sc dir interp (patl,uninterp,b) =
+  register_string_interpretation sc (interp,uninterp);
+  enable_prim_token_interpretation
+    { pt_scope = sc;
+      pt_uid = sc;
+      pt_required = dir;
+      pt_refs = List.map_filter glob_prim_constr_key patl;
+      pt_in_match = b }
+
 
 let check_required_module ?loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
@@ -468,14 +570,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 in
+  let (spdir,uid) = String.Map.find sc !prim_token_interp_infos in
   check_required_module ?loc sc spdir;
-  let pat =
-    match p, interp with
-    | Numeral (n,s), ForNumeral interp -> interp ?loc (n,s)
-    | String s, ForString interp -> interp ?loc s
-    | _ -> raise Not_found
-  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),"")
 
@@ -646,32 +744,33 @@ 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
+  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 =
-    match n, Hashtbl.find prim_token_interpreter_tab scope with
-    | exception Not_found -> false
-    | Numeral _, (_,ForNumeral _) -> true
-    | String _, (_,ForString _) -> true
-    | _ -> false
+    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)
@@ -1193,16 +1292,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
@@ -1211,7 +1313,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 e8408330af..2545e494ef 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,61 @@ 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
 
-val declare_rawnumeral_interpreter : scope_name -> required_module ->
-  rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit
+type 'a prim_token_interpretation =
+  'a prim_token_interpreter * 'a prim_token_uninterpreter
 
-val declare_numeral_interpreter : scope_name -> required_module ->
-  bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit
+val register_rawnumeral_interpretation :
+  prim_token_uid -> rawnum prim_token_interpretation -> unit
+
+val register_bignumeral_interpretation :
+  prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit
+
+val register_string_interpretation :
+  prim_token_uid -> string prim_token_interpretation -> unit
+
+type prim_token_infos = {
+  pt_scope : scope_name; (** Concerned scope *)
+  pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
+  pt_required : required_module; (** Module that should be loaded first *)
+  pt_refs : global_reference list; (** Entry points during uninterpretation *)
+  pt_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 enable_prim_token_interpretation : prim_token_infos -> 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_numeral_interpreter : scope_name -> required_module ->
+  Bigint.bigint prim_token_interpreter ->
+  glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit
 val declare_string_interpreter : scope_name -> required_module ->
-  string prim_token_interpreter -> string prim_token_uninterpreter -> unit
+  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*)
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 47a59ba631..9bf0b29b61 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -83,8 +83,17 @@ 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_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/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index f10f98e23b..731eae349a 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -96,10 +96,18 @@ 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_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
index 0e202be47f..29b88b1cb3 100644
--- a/plugins/syntax/n_syntax.ml
+++ b/plugins/syntax/n_syntax.ml
@@ -72,10 +72,17 @@ let uninterp_n (AnyGlobConstr p) =
 (************************************************************************)
 (* 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)
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
+let _ =
+  let scope = "N_scope" in
+  register_bignumeral_interpretation scope (n_of_int,uninterp_n);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_scope = scope;
+      pt_uid = scope;
+      pt_required = (n_path,binnums);
+      pt_refs = [glob_N0; glob_Npos];
+      pt_in_match = true }
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index e158e0b516..85cb49586d 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -78,8 +78,18 @@ let uninterp_nat (AnyGlobConstr p) =
 (************************************************************************)
 (* Declare the primitive parsers and printers *)
 
+open Notation
+
+let nat_scope = "nat_scope"
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
 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)
+  register_bignumeral_interpretation nat_scope (nat_of_int,uninterp_nat);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_scope = nat_scope;
+      pt_uid = nat_scope;
+      pt_required = (nat_path,datatypes_module_name);
+      pt_refs = [glob_S; glob_O];
+      pt_in_match = true }
diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml
index 0c82e47445..6fce4de9ef 100644
--- a/plugins/syntax/positive_syntax.ml
+++ b/plugins/syntax/positive_syntax.ml
@@ -91,11 +91,17 @@ let uninterp_positive (AnyGlobConstr p) =
 (* 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)
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
+let _ =
+  let scope = "positive_scope" in
+  register_bignumeral_interpretation scope (interp_positive,uninterp_positive);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_scope = scope;
+      pt_uid = scope;
+      pt_required = (positive_path,binnums);
+      pt_refs = [glob_xI; glob_xO; glob_xH];
+      pt_in_match = true }
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 94aa143350..eccc544e41 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -131,9 +131,18 @@ 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_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..ca1bf0df27 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -64,10 +64,17 @@ 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_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
index 2534162e36..72e1321eab 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -68,11 +68,17 @@ let uninterp_z (AnyGlobConstr p) =
 (************************************************************************)
 (* 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)
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
+let _ =
+  let scope = "Z_scope" in
+  register_bignumeral_interpretation scope (z_of_int,uninterp_z);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_scope = scope;
+      pt_uid = scope;
+      pt_required = (z_path,binnums);
+      pt_refs = [glob_ZERO; glob_POS; glob_NEG];
+      pt_in_match = true }
diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v
new file mode 100644
index 0000000000..ca8cba67d5
--- /dev/null
+++ b/test-suite/interactive/PrimNotation.v
@@ -0,0 +1,18 @@
+(* 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 0.
+(* 0 : nat *)
+Require BinNums.
+Check 0.
+(* 0 : BinNums.Z *)
+Back 2.
+Check 0.
+(* Expected answer: 0 : nat *)
+(* Used to fail with:
+Error: Cannot interpret in Z_scope without requiring first module BinNums.
+*)