diff options
Diffstat (limited to 'backend/Unusedglobproof.v')
-rw-r--r-- | backend/Unusedglobproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 7899a04c..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: @@ -1373,9 +1373,9 @@ Proof. * apply Y with id; auto. * exists gd1; auto. * exists gd2; auto. - * eapply used_not_defined_2 in GD1; eauto. eapply used_not_defined_2 in GD2; eauto. + * eapply used_not_defined_2 in GD1; [ | eauto | congruence ]. + eapply used_not_defined_2 in GD2; [ | eauto | congruence ]. tauto. - congruence. } destruct E as [g LD]. left. unfold prog_defs_names; simpl. |