diff options
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 6b1f2232..ea6f5c92 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -87,6 +87,7 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]) *) +Declare Scope asm. Notation "'SP'" := GPR1 (only parsing) : asm. Notation "'RA'" := LR (only parsing) : asm. |