6 files changed, 9 insertions, 35 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 5e36fbeb81..53153198f9 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -94,7 +94,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = sc;
-      pt_uid = sc;
+      pt_interp_info = 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
index 68b8178368..55f61a58f9 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -10,8 +10,8 @@
 
 DECLARE PLUGIN "numeral_notation_plugin"
 
-open Numeral
 open Notation
+open Numeral
 open Pp
 open Names
 open Vernacinterp
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index d3ffe936a9..e34a401c2c 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -108,7 +108,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = int31_scope;
-      pt_uid = int31_scope;
+      pt_interp_info = Uid int31_scope;
       pt_required = (int31_path,int31_module);
       pt_refs = [int31_construct];
       pt_in_match = true }
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 1a70c9536d..10a0af0b8f 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -27,29 +27,6 @@ let warn_abstract_large_num_no_op =
       Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
       strbrk "option type.")
 
-(* 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 (Notation.Numeral.interp opts, Notation.Numeral.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
@@ -154,15 +131,12 @@ let vernac_numeral_notation local ty f g scope opts =
   (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.(
+  let i =
        { pt_local = local;
          pt_scope = scope;
-         pt_uid = uid;
+         pt_interp_info = NumeralNotation o;
          pt_required = Nametab.path_of_global (IndRef tyc),[];
          pt_refs = constructors;
-         pt_in_match = true })
+         pt_in_match = true }
   in
-  Lib.add_anonymous_leaf (inNumeralNotation (uid,o));
-  Notation.enable_prim_token_interpretation i
+  enable_prim_token_interpretation i
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 04946c158b..49497aef54 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -143,7 +143,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = r_scope;
-      pt_uid = r_scope;
+      pt_interp_info = 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 640bcfde91..7478c1e978 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -75,7 +75,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = sc;
-      pt_uid = sc;
+      pt_interp_info = Uid sc;
       pt_required = (string_path,["Coq";"Strings";"String"]);
       pt_refs = [static_glob_String; static_glob_EmptyString];
       pt_in_match = true }