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.

1 files changed, 1 insertions, 1 deletions

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 }