diff options
Diffstat (limited to 'ia32/Asm.v')
-rw-r--r-- | ia32/Asm.v | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -70,7 +70,7 @@ Coercion CR: crbit >-> preg. (** Conventional names for stack pointer ([SP]) and return address ([RA]) *) -Notation "'SP'" := ESP (only parsing). +Notation SP := ESP (only parsing). (** ** Instruction set. *) |