diff options
Diffstat (limited to 'powerpc/Asmgenproof.v')
| -rw-r--r-- | powerpc/Asmgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 37c8808..e723c86 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -903,7 +903,7 @@ Local Transparent destroyed_by_jumptable. intros [m1' [C D]]. exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. - simpl Mach.chunk_of_type in F. + simpl chunk_of_type in F. exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. intros [m3' [P Q]]. (* Execution of function prologue *) |