Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp

1 files changed, 3 insertions, 3 deletions

diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 6d83cf5a..0be56e47 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -1258,11 +1258,11 @@ 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 *)
-  7,8,15,16:
+  7,14:
     econstructor; split; try apply exec_straight_one; simpl; eauto;
-    split; intros; Simpl; unfold may_undef_int; try destruct is_long; simpl;
+    split; intros; Simpl; simpl;
     try rewrite Int.add_commut; try rewrite Int64.add_commut;
-    destruct (rs (preg_of m0)); try discriminate; eauto.
+    auto.
   1-12:
     destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
     econstructor; split; try apply exec_straight_one; simpl; eauto;