diff options
Diffstat (limited to 'aarch64/Asm.v')
| -rw-r--r-- | aarch64/Asm.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index c5f4032e..0b5b01b8 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -96,6 +96,7 @@ Coercion preg_of_iregsp: iregsp >-> preg. (** Conventional name for return address ([RA]) *) +Declare Scope asm. Notation "'RA'" := X30 (only parsing) : asm. (** The instruction set. Most instructions correspond exactly to |