diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 26d3d347..2dd34389 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -1055,7 +1055,7 @@ Proof. assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty). replace (sizeof tge ty) with (Z.of_nat (List.length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. - rewrite LEN. apply nat_of_Z_eq. omega. + rewrite LEN. apply Z2Nat.id. omega. assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty). apply RPSRC. omega. assert (PDST: Mem.perm m bdst (Ptrofs.unsigned odst) Cur Nonempty). |