From e9d44aefa9d6058c72845788745468aa010708b5 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 23 Aug 2018 15:10:58 -0400
Subject: Make Numeral Notation obey Local/Global

Thanks to Emilio and Pierre-Marie Pédrot for pointers.
---
 plugins/syntax/string_syntax.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/syntax/string_syntax.ml')

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];
-- 
cgit v1.2.3