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/r_syntax.ml b/plugins/syntax/r_syntax.ml
index eccc544e41..04946c158b 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -141,7 +141,8 @@ let r_scope = "R_scope"
 let _ =
   register_bignumeral_interpretation r_scope (r_of_int,uninterp_r);
   at_declare_ml_module enable_prim_token_interpretation
-    { pt_scope = r_scope;
+    { pt_local = false;
+      pt_scope = r_scope;
       pt_uid = r_scope;
       pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
       pt_refs = [glob_IZR];