Give explicit scopes to notations a#b and a##b and a#b<-c

Without scopes Coq 8.6 warns, probably rightly so.

4 files changed, 21 insertions, 13 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index d211ead0..bc5ca1a5 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -84,8 +84,8 @@ Module Pregmap := EMap(PregEq).
 
 (** Conventional names for stack pointer ([SP]) and return address ([RA]) *)
 
-Notation "'SP'" := IR13 (only parsing).
-Notation "'RA'" := IR14 (only parsing).
+Notation "'SP'" := IR13 (only parsing) : asm.
+Notation "'RA'" := IR14 (only parsing) : asm.
 
 (** The instruction set.  Most instructions correspond exactly to
   actual instructions of the ARM processor. See the ARM
@@ -294,8 +294,10 @@ Definition program := AST.program fundef unit.
 Definition regset := Pregmap.t val.
 Definition genv := Genv.t fundef unit.
 
-Notation "a # b" := (a b) (at level 1, only parsing).
-Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level).
+Notation "a # b" := (a b) (at level 1, only parsing) : asm.
+Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
+
+Open Scope asm.
 
 (** Undefining some registers *)
 
diff --git a/backend/Registers.v b/backend/Registers.v
index cfe8427b..622cddfe 100644
--- a/backend/Registers.v
+++ b/backend/Registers.v
@@ -61,9 +61,11 @@ Definition regmap_setres
   | _ => rs
   end.
 
-Notation "a # b" := (Regmap.get b a) (at level 1).
-Notation "a ## b" := (List.map (fun r => Regmap.get r a) b) (at level 1).
-Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level).
+Notation "a # b" := (Regmap.get b a) (at level 1) : rtl.
+Notation "a ## b" := (List.map (fun r => Regmap.get r a) b) (at level 1) : rtl.
+Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level) : rtl.
+
+Open Scope rtl.
 
 (** Pointwise "less defined than" relation between register maps. *)
 
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 3c269083..cc554eb1 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -87,8 +87,8 @@ Module Pregmap := EMap(PregEq).
 
 (** Conventional names for stack pointer ([SP]) and return address ([RA]) *)
 
-Notation "'SP'" := GPR1 (only parsing).
-Notation "'RA'" := LR (only parsing).
+Notation "'SP'" := GPR1 (only parsing) : asm.
+Notation "'RA'" := LR (only parsing) : asm.
 
 (** Symbolic constants.  Immediate operands to an arithmetic instruction
   or an indexed memory access can be either integer literals,
@@ -385,8 +385,10 @@ Definition program := AST.program fundef unit.
 Definition regset := Pregmap.t val.
 Definition genv := Genv.t fundef unit.
 
-Notation "a # b" := (a b) (at level 1, only parsing).
-Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level).
+Notation "a # b" := (a b) (at level 1, only parsing) : asm.
+Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
+
+Open Scope asm.
 
 (** Undefining some registers *)
 
diff --git a/x86/Asm.v b/x86/Asm.v
index 304cb8e4..1c204b02 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -310,8 +310,10 @@ Module Pregmap := EMap(PregEq).
 Definition regset := Pregmap.t val.
 Definition genv := Genv.t fundef unit.
 
-Notation "a # b" := (a b) (at level 1, only parsing).
-Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level).
+Notation "a # b" := (a b) (at level 1, only parsing) : asm.
+Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
+
+Open Scope asm.
 
 (** Undefining some registers *)