diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-23 14:12:04 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-23 14:12:04 +0200 |
| commit | b66ddea9b0304d390b56afadda80fa4d2f2184d6 (patch) | |
| tree | 27a2ad0533fcd52a0d82b92ea3f582a3c02065d9 /cfrontend | |
| parent | 23f871b3faf89679414485c438ed211151bd99ce (diff) | |
| download | compcert-kvx-b66ddea9b0304d390b56afadda80fa4d2f2184d6.tar.gz compcert-kvx-b66ddea9b0304d390b56afadda80fa4d2f2184d6.zip | |
Replace nat_of_Z with Z.to_nat
Use Z.to_nat theorems from the standard Coq library in preference to
our theorems in lib/Coqlib.v.
Simplify lib/Coqlib.v accordingly.
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). |