diff options
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index e58c7f0c..7da86de4 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1639,10 +1639,9 @@ Opaque Int.eq. exists rs'; split. eexact A. eauto with asmgen. - (* Oselect *) destruct cond in *; simpl in *; try congruence; injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in *; - econstructor; split. - - + eapply exec_straight_one. - simpl; reflexivity. + econstructor; split; + try ( eapply exec_straight_one; + simpl; reflexivity ). + split. * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. @@ -1652,8 +1651,6 @@ Opaque Int.eq. destruct b; simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. - + eapply exec_straight_one. - simpl; reflexivity. + split. * unfold eval_select. destruct (rs x) eqn:eqX; try constructor. |