diff options
Diffstat (limited to 'riscV/Asmgenproof1.v')
| -rw-r--r-- | riscV/Asmgenproof1.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index cbe68577..2293e001 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1274,7 +1274,7 @@ Opaque Int.eq. { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) - 8,9,17,18: + 9,10,19,20: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; try destruct (rs x0); try rewrite Int64.add_commut; @@ -1283,9 +1283,8 @@ Opaque Int.eq. try rewrite Int.and_commut; auto; try rewrite Int64.or_commut; try rewrite Int.or_commut; auto. - 1-14: + 1-16: destruct optR as [[]|]; try discriminate; - try (ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl); unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; try inv EQ3; try inv EQ2; try destruct (Int.eq _ _) eqn:A; try inv H0; try destruct (Int64.eq _ _) eqn:A; try inv H1; |