diff options
Diffstat (limited to 'backend/Allocproof.v')
| -rw-r--r-- | backend/Allocproof.v | 17 |
1 files changed, 4 insertions, 13 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index ae86ee8b..a9477e02 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -705,22 +705,13 @@ Proof. eapply agree_assign_live; eauto. eapply agree_reg_list_live; eauto. - (* Icond, true *) - assert (COND: eval_condition cond (map ls (map assign args)) m = Some true). + (* Icond *) + assert (COND: eval_condition cond (map ls (map assign args)) m = Some b). replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. - eapply exec_Lcond_true; eauto. TranslInstr. - MatchStates. - eapply agree_undef_temps; eauto. - eapply agree_reg_list_live. eauto. - (* Icond, false *) - assert (COND: eval_condition cond (map ls (map assign args)) m = Some false). - replace (map ls (map assign args)) with (rs##args). auto. - eapply agree_eval_regs; eauto. - econstructor; split. - eapply exec_Lcond_false; eauto. TranslInstr. - MatchStates. + eapply exec_Lcond; eauto. TranslInstr. + MatchStates. destruct b; simpl; auto. eapply agree_undef_temps; eauto. eapply agree_reg_list_live. eauto. |