Now a more general way to perform imm operations

1 files changed, 6 insertions, 1 deletions

diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 639c9a64..6e5cc531 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -1258,7 +1258,12 @@ 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,9,10,17,18,19,20:
+  { unfold get_opimmR0; destruct opi; simpl;
+    econstructor; split; try apply exec_straight_one; simpl; eauto;
+    split; intros; Simpl.
+    try rewrite Int.add_commut; auto.
+    try rewrite Int64.add_commut; auto. }
+  7,8,9,16,17,18:
     econstructor; split; try apply exec_straight_one; simpl; eauto;
     split; intros; Simpl; try destruct (rs x0);
     try rewrite Int64.add_commut;