Make Numeral Notation obey Local/Global

Thanks to Emilio and Pierre-Marie Pédrot for pointers.

1 files changed, 2 insertions, 1 deletions

diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index ca1bf0df27..640bcfde91 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -73,7 +73,8 @@ let _ =
   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_local = false;
+      pt_scope = sc;
       pt_uid = sc;
       pt_required = (string_path,["Coq";"Strings";"String"]);
       pt_refs = [static_glob_String; static_glob_EmptyString];