1 files changed, 1 insertions, 1 deletions
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 87d9dc9f..df901db5 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -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. *)