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 /backend/CSEproof.v | |
parent | 23f871b3faf89679414485c438ed211151bd99ce (diff) | |
download | compcert-b66ddea9b0304d390b56afadda80fa4d2f2184d6.tar.gz compcert-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 'backend/CSEproof.v')
-rw-r--r-- | backend/CSEproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index d6bde348..a60c316b 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -544,7 +544,7 @@ Lemma kill_loads_after_storebytes_holds: bc sp = BCstack -> ematch bc rs ae -> approx = VA.State ae am -> - length bytes = nat_of_Z sz -> sz >= 0 -> + length bytes = Z.to_nat sz -> sz >= 0 -> numbering_holds valu ge (Vptr sp Ptrofs.zero) rs m' (kill_loads_after_storebytes approx n dst sz). Proof. @@ -557,7 +557,7 @@ Proof. simpl. rewrite negb_false_iff in H8. eapply Mem.load_storebytes_other. eauto. - rewrite H6. rewrite nat_of_Z_eq by auto. + rewrite H6. rewrite Z2Nat.id by omega. eapply pdisjoint_sound. eauto. unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. @@ -598,9 +598,9 @@ Proof. exploit Mem.storebytes_split; eauto. intros (m2 & SB2 & SB3). clear SB23. assert (L1: Z.of_nat (length bytes1) = n1). - { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n1; omega. } + { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n1; omega. } assert (L2: Z.of_nat (length bytes2) = n2). - { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n2; omega. } + { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n2; omega. } rewrite L1 in *. rewrite L2 in *. assert (LB': Mem.loadbytes m2 b2 (ofs2 + n1) n2 = Some bytes2). { rewrite <- L2. eapply Mem.loadbytes_storebytes_same; eauto. } |