Make Numeral Notation obey Local/Global

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

7 files changed, 15 insertions, 8 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 9bf0b29b61..5e36fbeb81 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -92,7 +92,8 @@ let _ =
   let sc = "char_scope" in
   register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string);
   at_declare_ml_module enable_prim_token_interpretation
-    { pt_scope = sc;
+    { pt_local = false;
+      pt_scope = sc;
       pt_uid = sc;
       pt_required = (ascii_path,ascii_module);
       pt_refs = [static_glob_Ascii];
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index 4e29e6a6a4..ec14df3baa 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -13,6 +13,7 @@ DECLARE PLUGIN "numeral_notation_plugin"
 open Numeral
 open Pp
 open Names
+open Vernacinterp
 open Ltac_plugin
 open Stdarg
 open Pcoq.Prim
@@ -32,5 +33,5 @@ END
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
   | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) numnotoption(o) ] ->
-    [ vernac_numeral_notation ty f g (Id.to_string sc) o ]
+    [ vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o ]
 END
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index 731eae349a..d3ffe936a9 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -106,7 +106,8 @@ let at_declare_ml_module f x =
 let _ =
   register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31);
   at_declare_ml_module enable_prim_token_interpretation
-    { pt_scope = int31_scope;
+    { pt_local = false;
+      pt_scope = int31_scope;
       pt_uid = int31_scope;
       pt_required = (int31_path,int31_module);
       pt_refs = [int31_construct];
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 321992eda6..fee93593d0 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -411,7 +411,7 @@ let type_error_of g ty loadZ =
      str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++
      (if loadZ then str " (require BinNums first)." else str "."))
 
-let vernac_numeral_notation ty f g scope opts =
+let vernac_numeral_notation local ty f g scope opts =
   let int_ty = locate_int () in
   let z_pos_ty = locate_z () in
   let tyc = Smartlocate.global_inductive_with_alias ty in
@@ -467,7 +467,8 @@ let vernac_numeral_notation ty f g scope opts =
   (* TODO: un hash suffit-il ? *)
   let uid = Marshal.to_string o [] in
   let i = Notation.(
-       { pt_scope = scope;
+       { pt_local = local;
+         pt_scope = scope;
          pt_uid = uid;
          pt_required = Nametab.path_of_global (IndRef tyc),[];
          pt_refs = constructors;
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 2ad3574fe7..83ede6f48f 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -10,6 +10,7 @@
 
 open Libnames
 open Constrexpr
+open Vernacexpr
 
 (** * Numeral notation *)
 
@@ -18,4 +19,4 @@ type numnot_option =
   | Warning of raw_natural_number
   | Abstract of raw_natural_number
 
-val vernac_numeral_notation : qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
+val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
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];
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];