diff options
Diffstat (limited to 'arm/Asmgenproof.v')
| -rw-r--r-- | arm/Asmgenproof.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 92ae524f..fd70c9ad 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -225,7 +225,7 @@ Proof. TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. Qed. -Hint Resolve indexed_memory_access_label. +Hint Resolve indexed_memory_access_label: labels. Remark loadind_label: forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> tail_nolabel k c. @@ -761,13 +761,15 @@ Opaque loadind. econstructor; eauto. instantiate (2 := tf); instantiate (1 := x). unfold nextinstr. rewrite Pregmap.gss. - rewrite set_res_other. rewrite undef_regs_other_2. + rewrite set_res_other. simpl. rewrite undef_regs_other_2. + rewrite Pregmap.gso by auto with asmgen. rewrite <- H1. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. rewrite preg_notin_charact. intros. auto with asmgen. auto with asmgen. apply agree_nextinstr. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. + eapply agree_undef_regs; eauto. + intros. simpl. rewrite undef_regs_other_2; auto. apply Pregmap.gso. auto with asmgen. congruence. - (* Mgoto *) |