Partial backtracking on previous commit: the "hole in Mach stack frame"

trick prevents a future mapping of the Mach/Asm call stack as a single
block.  IA32 is fixed, PowerPC and ARM remains to be done.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2136 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 1 insertions, 1 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 87d9dc9..df901db 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. *)