Fix Numeral Notations (4/4 - fixing synch)

This fixes #8401
Supersedes / closes #8407

Vernacular-command-registered numeral notations now live in the summary,
and the interpretation function for them is hard-coded.

Plugin-registered numeral notations are still unsynchronized, and only
the UIDs of these functions gets synchronized.  I am not 100% sure why
this is fine, but the test-suite file working suggests that it is fine.
I think it is because worker delegation correctly handles
non-synchronized state which is declared at `Declare ML Module`-time.

This final commit changes the synchronization of numeral notations (and
deletes no-longer-used declarations in notation.mli that were introduced
temporarily in the last commit).  Since the interpretation can now be
done in notation.ml, we no longer need to register unique ids for
numeral notation (un)interp functions, and can instead synchronize the
underlying constants with the document state.  This is the change that
actually fixes #8401.

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 }