diff options
Diffstat (limited to 'backend/Unusedglobproof.v')
| -rw-r--r-- | backend/Unusedglobproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index d5f871a0..680daba7 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -1160,10 +1160,10 @@ Local Transparent Mem.loadbytes. generalize (S1 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E1; inv E1. generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2. rewrite Z.add_0_r. - apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))). + apply Mem_getN_forall2 with (p := 0) (n := Z.to_nat (init_data_list_size (gvar_init v))). rewrite H3, H4. apply bytes_of_init_inject. auto. omega. - rewrite nat_of_Z_eq by (apply init_data_list_size_pos). omega. + rewrite Z2Nat.id by (apply Z.ge_le; apply init_data_list_size_pos). omega. Qed. Lemma init_mem_inj_2: |