diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-26 15:46:54 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-26 15:46:54 +0000 |
| commit | ad12162ff1f0d50c43afefc45e1593f27f197402 (patch) | |
| tree | f77430a75e0a4bf12a64b8ee676d40c88ede1041 /ia32/Asmgenproof1.v | |
| parent | 9fb435abe98f358b1dde5de6604663a176634e53 (diff) | |
Future-proofing: keep signature information in IA32 and PowerPC Asm, just like we already do in ARM Asm.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asmgenproof1.v')
| -rw-r--r-- | ia32/Asmgenproof1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 9ddc463..5d3df67 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -97,7 +97,7 @@ Ltac Simplifs := repeat Simplif. Section CONSTRUCTORS. Variable ge: genv. -Variable fn: code. +Variable fn: function. (** Smart constructor for moves. *) |