Merge conflicts solved and cleaning in Asmgenproof after expansion

4 files changed, 106 insertions, 1148 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 252a9270..957166b6 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -105,8 +105,6 @@ Definition addimm32 := opimm32 Paddw Paddiw.
 Definition andimm32 := opimm32 Pandw Pandiw.
 Definition orimm32  := opimm32 Porw  Poriw.
 Definition xorimm32 := opimm32 Pxorw Pxoriw.
-Definition sltimm32 := opimm32 Psltw Psltiw.
-Definition sltuimm32 := opimm32 Psltuw Psltiuw.
   
 Definition load_hilo64 (r: ireg) (hi lo: int64) k :=
   if Int64.eq lo Int64.zero then Pluil r hi :: k
@@ -132,8 +130,6 @@ Definition addimm64 := opimm64 Paddl Paddil.
 Definition andimm64 := opimm64 Pandl Pandil.
 Definition orimm64  := opimm64 Porl  Poril.
 Definition xorimm64 := opimm64 Pxorl  Pxoril.
-Definition sltimm64 := opimm64 Psltl Psltil.
-Definition sltuimm64 := opimm64 Psltul Psltiul.
 
 Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
@@ -145,66 +141,6 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   
 (** Translation of conditional branches. *)
 
-Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeqw r1 r2 lbl
-  | Cne => Pbnew r1 r2 lbl
-  | Clt => Pbltw r1 r2 lbl
-  | Cle => Pbgew r2 r1 lbl
-  | Cgt => Pbltw r2 r1 lbl
-  | Cge => Pbgew r1 r2 lbl
-  end.
-
-Definition transl_cbranch_int32u (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeqw  r1 r2 lbl
-  | Cne => Pbnew  r1 r2 lbl
-  | Clt => Pbltuw r1 r2 lbl
-  | Cle => Pbgeuw r2 r1 lbl
-  | Cgt => Pbltuw r2 r1 lbl
-  | Cge => Pbgeuw r1 r2 lbl
-  end.
-
-Definition transl_cbranch_int64s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeql r1 r2 lbl
-  | Cne => Pbnel r1 r2 lbl
-  | Clt => Pbltl r1 r2 lbl
-  | Cle => Pbgel r2 r1 lbl
-  | Cgt => Pbltl r2 r1 lbl
-  | Cge => Pbgel r1 r2 lbl
-  end.
-
-Definition transl_cbranch_int64u (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
-  match cmp with
-  | Ceq => Pbeql  r1 r2 lbl
-  | Cne => Pbnel  r1 r2 lbl
-  | Clt => Pbltul r1 r2 lbl
-  | Cle => Pbgeul r2 r1 lbl
-  | Cgt => Pbltul r2 r1 lbl
-  | Cge => Pbgeul r1 r2 lbl
-  end.
-
-Definition transl_cond_float (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
-  match cmp with
-  | Ceq => (Pfeqd rd fs1 fs2, true)
-  | Cne => (Pfeqd rd fs1 fs2, false)
-  | Clt => (Pfltd rd fs1 fs2, true)
-  | Cle => (Pfled rd fs1 fs2, true)
-  | Cgt => (Pfltd rd fs2 fs1, true)
-  | Cge => (Pfled rd fs2 fs1, true)
-  end.
-  
-Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
-  match cmp with
-  | Ceq => (Pfeqs rd fs1 fs2, true)
-  | Cne => (Pfeqs rd fs1 fs2, false)
-  | Clt => (Pflts rd fs1 fs2, true)
-  | Cle => (Pfles rd fs1 fs2, true)
-  | Cgt => (Pflts rd fs2 fs1, true)
-  | Cge => (Pfles rd fs2 fs1, true)
-   end.
- 
 Definition apply_bin_r0_r0r0lbl (optR0: option bool) (sem: ireg0 -> ireg0 -> label -> instruction) (r1 r2: ireg0) (lbl: label) :=
   match optR0 with
   | None => sem r1 r2 lbl
@@ -222,59 +158,6 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru
 Definition transl_cbranch
            (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
   match cond, args with
-  | Ccomp c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int32s c r1 r2 lbl :: k)
-  | Ccompu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int32u c r1 r2 lbl :: k)
-  | Ccompimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int.eq n Int.zero then
-            transl_cbranch_int32s c r1 X0 lbl :: k
-          else
-            loadimm32 X31 n (transl_cbranch_int32s c r1 X31 lbl :: k))
-  | Ccompuimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int.eq n Int.zero then
-            transl_cbranch_int32u c r1 X0 lbl :: k
-          else
-            loadimm32 X31 n (transl_cbranch_int32u c r1 X31 lbl :: k))
-  | Ccompl c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int64s c r1 r2 lbl :: k)
-  | Ccomplu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cbranch_int64u c r1 r2 lbl :: k)
-  | Ccomplimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int64.eq n Int64.zero then
-            transl_cbranch_int64s c r1 X0 lbl :: k
-          else
-            loadimm64 X31 n (transl_cbranch_int64s c r1 X31 lbl :: k))
-  | Ccompluimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int64.eq n Int64.zero then
-            transl_cbranch_int64u c r1 X0 lbl :: k
-          else
-            loadimm64 X31 n (transl_cbranch_int64u c r1 X31 lbl :: k))
-  | Ccompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c X31 r1 r2 in
-      OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k)
-  | Cnotcompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c X31 r1 r2 in
-      OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
-  | Ccompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c X31 r1 r2 in
-      OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k)
-  | Cnotcompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c X31 r1 r2 in
-   OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
-
   | CEbeqw optR0, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k)
@@ -327,133 +210,6 @@ Definition transl_cbranch
       Error(msg "Asmgen.transl_cond_branch")
   end.
 
-(** Translation of a condition operator.  The generated code sets the
-  [rd] target register to 0 or 1 depending on the truth value of the
-  condition. *)
-
-Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
-  match cmp with
-  | Ceq => Pseqw rd r1 r2 :: k
-  | Cne => Psnew rd r1 r2 :: k
-  | Clt => Psltw rd r1 r2 :: k
-  | Cle => Psltw rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltw rd r2 r1 :: k
-  | Cge => Psltw rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_cond_int32u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
-  match cmp with
-  | Ceq => Pseqw rd r1 r2 :: k
-  | Cne => Psnew rd r1 r2 :: k
-  | Clt => Psltuw rd r1 r2 :: k
-  | Cle => Psltuw rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltuw rd r2 r1 :: k
-  | Cge => Psltuw rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_cond_int64s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
-  match cmp with
-  | Ceq => Pseql rd r1 r2 :: k
-  | Cne => Psnel rd r1 r2 :: k
-  | Clt => Psltl rd r1 r2 :: k
-  | Cle => Psltl rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltl rd r2 r1 :: k
-  | Cge => Psltl rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_cond_int64u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
-  match cmp with
-  | Ceq => Pseql rd r1 r2 :: k
-  | Cne => Psnel rd r1 r2 :: k
-  | Clt => Psltul rd r1 r2 :: k
-  | Cle => Psltul rd r2 r1 :: Pxoriw rd rd Int.one :: k
-  | Cgt => Psltul rd r2 r1 :: k
-  | Cge => Psltul rd r1 r2 :: Pxoriw rd rd Int.one :: k
-  end.
-
-Definition transl_condimm_int32s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
-  if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 X0 k else
-  match cmp with
-  | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd X0 k)
-  | Clt => sltimm32 rd r1 n k
-  | Cle => if Int.eq n (Int.repr Int.max_signed)
-           then loadimm32 rd Int.one k
-           else sltimm32 rd r1 (Int.add n Int.one) k
-  | _   => loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)
-  end.
-
-Definition transl_condimm_int32u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
-  if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 X0 k else
-  match cmp with
-  | Clt => sltuimm32 rd r1 n k
-  | _   => loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)
-  end.
-
-Definition transl_condimm_int64s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
-  if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 X0 k else
-  match cmp with
-  | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd X0 k)
-  | Clt => sltimm64 rd r1 n k
-  | Cle => if Int64.eq n (Int64.repr Int64.max_signed)
-           then loadimm32 rd Int.one k
-           else sltimm64 rd r1 (Int64.add n Int64.one) k
-  | _   => loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)
-  end.
-
-Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
-  if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 X0 k else
-  match cmp with
-  | Clt => sltuimm64 rd r1 n k
-  | _   => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
-   end.
-
-Definition transl_cond_op
-           (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
-  match cond, args with
-  | Ccomp c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int32s c rd r1 r2 k)
-  | Ccompu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int32u c rd r1 r2 k)
-  | Ccompimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int32s c rd r1 n k)
-  | Ccompuimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int32u c rd r1 n k)
-  | Ccompl c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int64s c rd r1 r2 k)
-  | Ccomplu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-     OK (transl_cond_int64u c rd r1 r2 k)
-  | Ccomplimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int64s c rd r1 n k)
-  | Ccompluimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-     OK (transl_condimm_int64u c rd r1 n k)
-  | Ccompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-  | Ccompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-     OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-  | _, _ =>
-      Error(msg "Asmgen.transl_cond_op")
-   end.
-
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
   
@@ -767,9 +523,6 @@ Definition transl_op
   | Osingleoflongu, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfcvtslu rd rs :: k)
-  | Ocmp cmp, _ =>
-      do rd <- ireg_of res;
-     transl_cond_op cmp rd args k
   | OEseqw optR0, a1 :: a2 :: nil =>
       do rd <- ireg_of res;
       do rs1 <- ireg_of a1;
@@ -912,18 +665,12 @@ Definition transl_op
   | Ofloat_of_bits, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfmvdx rd rs :: k)
-                               
-  | Ocmp cmp, _ =>
-      do rd <- ireg_of res;
-      transl_cond_op cmp rd args k
-
   | Oselectl, b::t::f::nil =>
       do rd <- ireg_of res;
       do rb <- ireg_of b;
       do rt <- ireg_of t;
       do rf <- ireg_of f;
       OK (Pselectl rd rb rt rf :: k)
-         
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 82c1917d..6abad4ed 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -161,165 +161,37 @@ Proof.
 Qed.
 Hint Resolve addptrofs_label: labels.
 
-Remark transl_cond_float_nolabel:
-  forall c r1 r2 r3 insn normal,
-  transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.
-Proof.
-  unfold transl_cond_float; intros. destruct c; inv H; exact I.
-Qed.
-
-Remark transl_cond_single_nolabel:
-  forall c r1 r2 r3 insn normal,
-  transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.
-Proof.
-  unfold transl_cond_single; intros. destruct c; inv H; exact I.
-   Qed.
-
 Remark transl_cbranch_label:
   forall cond args lbl k c,
   transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
 Proof.
   intros. unfold transl_cbranch in H; destruct cond; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct (Int.eq n Int.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int32s c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (Int.eq n Int.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int32u c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct (Int64.eq n Int64.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int64s c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (Int64.eq n Int64.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int64u c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-     destruct normal; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
-- destruct optR0 as [[]|]; TailNoLabel.
+  all:  destruct optR0 as [[]|]; TailNoLabel.
 Qed.
 
-Remark transl_cond_op_label:
-  forall cond args r k c,
-  transl_cond_op cond r args k = OK c -> tail_nolabel k c.
-Proof.
-  intros. unfold transl_cond_op in H; destruct cond; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel. 
-- unfold transl_condimm_int32s.
-  destruct (Int.eq n Int.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl.
-* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel].
-* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel].
-* apply opimm32_label; intros; exact I.
-* destruct (Int.eq n (Int.repr Int.max_signed)). apply loadimm32_label. apply opimm32_label; intros; exact I.
-* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel.
-* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel.
-- unfold transl_condimm_int32u.
-  destruct (Int.eq n Int.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl; 
-  try (eapply tail_nolabel_trans; [apply loadimm32_label | TailNoLabel]).
-  apply opimm32_label; intros; exact I.
-- destruct c0; simpl; TailNoLabel.
-     - destruct c0; simpl; TailNoLabel.
-- unfold transl_condimm_int64s.
-  destruct (Int64.eq n Int64.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl.
-* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel].
-* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel].
-* apply opimm64_label; intros; exact I.
-* destruct (Int64.eq n (Int64.repr Int64.max_signed)). apply loadimm32_label. apply opimm64_label; intros; exact I.
-* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel.
-* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel.
-- unfold transl_condimm_int64u.
-  destruct (Int64.eq n Int64.zero).
-+ destruct c0; simpl; TailNoLabel.
-+ destruct c0; simpl; 
-  try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]).
-     apply opimm64_label; intros; exact I.
-- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-   Qed.
-
 Remark transl_op_label:
   forall op args r k c,
   transl_op op args r k = OK c -> tail_nolabel k c.
 Proof.
 Opaque Int.eq.
   unfold transl_op; intros; destruct op; TailNoLabel.
-- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
-- destruct (Float.eq_dec n Float.zero); TailNoLabel.
-- destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
-- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
-+ eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
-+ TailNoLabel. 
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
-- eapply transl_cond_op_label; eauto.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
-- destruct optR0 as [[]|]; simpl; TailNoLabel.
+  { destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. }
+  { destruct (Float.eq_dec n Float.zero); TailNoLabel. }
+  { destruct (Float32.eq_dec n Float32.zero); TailNoLabel. }
+  { destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
+    + eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
+    + TailNoLabel. }
+  { apply opimm32_label; intros; exact I. }
+  { apply opimm32_label; intros; exact I. }
+  { apply opimm32_label; intros; exact I. }
+  { apply opimm32_label; intros; exact I. }
+  { destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. }
+  { apply opimm64_label; intros; exact I. }
+  { apply opimm64_label; intros; exact I. }
+  { apply opimm64_label; intros; exact I. }
+  { apply opimm64_label; intros; exact I. }
+  { destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. }
+  all: destruct optR0 as [[]|]; simpl; TailNoLabel.
 Qed.
 
 Remark indexed_memory_access_label:
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 1b3a0dbf..f0def29b 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -290,102 +290,6 @@ Proof.
   rewrite H0 in B. inv B. auto.
 Qed.
 
-(** Translation of conditional branches *)
-
-Lemma transl_cbranch_int32s_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmp_bool cmp rs##r1 rs##r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H.
-- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H.
-  simpl; auto.
-- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H.
-  simpl; auto.
-- auto.
-- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto.
-- auto.
-Qed.
-
-Lemma transl_cbranch_int32u_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int32u cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H; auto.
-- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto.
-Qed.
-
-Lemma transl_cbranch_int64s_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmpl_bool cmp rs###r1 rs###r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int64s cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H.
-- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H.
-  simpl; auto.
-- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H.
-  simpl; auto.
-- auto.
-- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto.
-- auto.
-Qed.
-
-Lemma transl_cbranch_int64u_correct:
-  forall cmp r1 r2 lbl (rs: regset) m b,
-  Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b ->
-  exec_instr ge fn (transl_cbranch_int64u cmp r1 r2 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct cmp; simpl; rewrite ? H; auto.
-- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto.
-- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto.
-Qed.
-
-Lemma transl_cond_float_correct:
-  forall (rs: regset) m cmp rd r1 r2 insn normal v,
-  transl_cond_float cmp rd r1 r2 = (insn, normal) ->
-  v = (if normal then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) ->
-  exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
-Proof.
-  intros. destruct cmp; simpl in H; inv H; auto. 
-- rewrite Val.negate_cmpf_eq. auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool.
-  rewrite <- Float.cmp_swap. auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool.
-  rewrite <- Float.cmp_swap. auto.
-Qed.
-
-Lemma transl_cond_single_correct:
-  forall (rs: regset) m cmp rd r1 r2 insn normal v,
-  transl_cond_single cmp rd r1 r2 = (insn, normal) ->
-  v = (if normal then Val.cmpfs cmp rs#r1 rs#r2 else Val.notbool (Val.cmpfs cmp rs#r1 rs#r2)) ->
-  exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m.
-Proof.
-  intros. destruct cmp; simpl in H; inv H; auto. 
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
-  rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f0 f); auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
-  rewrite <- Float32.cmp_swap. auto.
-- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool.
-  rewrite <- Float32.cmp_swap. auto.
-   Qed.
-
-(* TODO gourdinl UNUSUED ? Remark branch_on_X31:
-  forall normal lbl (rs: regset) m b,
-  rs#X31 = Val.of_bool (eqb normal b) -> 
-  exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m =
-  eval_branch fn lbl rs m (Some b).
-Proof.
-  intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. 
-   Qed.*)
-
 Ltac ArgsInv :=
   repeat (match goal with
   | [ H: Error _ = OK _ |- _ ] => discriminate
@@ -417,203 +321,84 @@ Proof.
   { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
   clear EVAL MEXT AG.
   destruct cond; simpl in TRANSL; ArgsInv.
-  - exists rs, (transl_cbranch_int32s c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
-- exists rs, (transl_cbranch_int32u c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
-- predSpec Int.eq Int.eq_spec n Int.zero.
-+ subst n. exists rs, (transl_cbranch_int32s c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32s_correct; auto.
-+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int32s c0 x X31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int32s_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- predSpec Int.eq Int.eq_spec n Int.zero.
-+ subst n. exists rs, (transl_cbranch_int32u c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int32u_correct; auto.
-+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int32u c0 x X31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int32u_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- exists rs, (transl_cbranch_int64s c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64s_correct; auto.
-- exists rs, (transl_cbranch_int64u c0 x x0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64u_correct; auto.
-- predSpec Int64.eq Int64.eq_spec n Int64.zero.
-+ subst n. exists rs, (transl_cbranch_int64s c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64s_correct; auto.
-+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int64s c0 x X31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int64s_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- predSpec Int64.eq Int64.eq_spec n Int64.zero.
-+ subst n. exists rs, (transl_cbranch_int64u c0 x X0 lbl).
-  intuition auto. constructor. apply transl_cbranch_int64u_correct; auto.
-+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C).
-  exists rs', (transl_cbranch_int64u c0 x X31 lbl).
-  split. constructor; eexact A. split; auto.
-  apply transl_cbranch_int64u_correct; auto.
-  simpl; rewrite B, C; eauto with asmgen.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (eqb normal b)).
-  { unfold v, Val.cmpf. rewrite EVAL'. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)).
-  { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. }
-  set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (xorb normal b)).
-  { unfold v, Val.cmpf. rewrite EVAL''. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (eqb normal b)).
-  { unfold v, Val.cmpfs. rewrite EVAL'. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-  intros; Simpl.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2.
-  assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)).
-  { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. }
-  set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)).
-  assert (V: v = Val.of_bool (xorb normal b)).
-  { unfold v, Val.cmpfs. rewrite EVAL''. destruct normal, b; reflexivity. }
-  econstructor; econstructor.
-  split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
-  split. rewrite V; destruct normal, b; reflexivity.
-     intros; Simpl.
-
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
-  eexists; eexists; eauto; split; constructor; auto;
-  simpl in *.
-  + destruct (rs x); simpl in *; try congruence.
-    assert (HB: (Int.eq Int.zero i) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
-    assert (HB: (Int.eq i Int.zero) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
-    destruct (rs x0); try congruence.
-    assert (HB: (Int.eq i i0) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
-  eexists; eexists; eauto; split; constructor; auto;
-  simpl in *.
-  + destruct (rs x); simpl in *; try congruence.
-    assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
-    assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
-    destruct (rs x0); try congruence.
-    assert (HB: negb (Int.eq i i0) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; auto.
-  + destruct (rs x); simpl in *; try congruence.
-    assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
-    assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
-    destruct (rs x0); try congruence.
-    assert (HB: (Int64.eq i i0) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; auto.
-  + destruct (rs x); simpl in *; try congruence.
-    assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
-    assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
-    destruct (rs x0); try congruence.
-    assert (HB: negb (Int64.eq i i0) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
-  eexists; eexists; eauto; split; constructor;
-  simpl in *; try rewrite EVAL'; auto.
+  (* Pbeqw / Cmp *)
+  { destruct optR0 as [[]|];
+    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+    unfold zero32, Op.zero32 in *;
+    eexists; eexists; eauto; split; constructor; auto;
+    simpl in *.
+    + destruct (rs x); simpl in *; try congruence.
+      assert (HB: (Int.eq Int.zero i) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto.
+    + destruct (rs x); simpl in *; try congruence.
+      assert (HB: (Int.eq i Int.zero) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto.
+    + destruct (rs x); simpl in *; try congruence.
+      destruct (rs x0); try congruence.
+      assert (HB: (Int.eq i i0) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto. }
+  (* Pbnew / Cmp *)
+  { destruct optR0 as [[]|];
+    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+    unfold zero32, Op.zero32 in *;
+    eexists; eexists; eauto; split; constructor; auto;
+    simpl in *.
+    + destruct (rs x); simpl in *; try congruence.
+      assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto.
+    + destruct (rs x); simpl in *; try congruence.
+      assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto.
+    + destruct (rs x); simpl in *; try congruence.
+      destruct (rs x0); try congruence.
+      assert (HB: negb (Int.eq i i0) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto. }
+  (* Pbeqw, Pbnew, Pbltw, Pbtluw, Pbgew, Pbgeuw / Cmpu *)
+  1-6:
+    destruct optR0 as [[]|];
+    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+    unfold zero32, Op.zero32 in *;
+    eexists; eexists; eauto; split; constructor;
+    simpl in *; try rewrite EVAL'; auto.
+  (* Pbeql / Cmpl *)
+  { destruct optR0 as [[]|];
+    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+    unfold zero64, Op.zero64 in *;
+    eexists; eexists; eauto; split; constructor;
+    simpl in *; auto.
+    + destruct (rs x); simpl in *; try congruence.
+      assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto.
+    + destruct (rs x); simpl in *; try congruence.
+      assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto.
+    + destruct (rs x); simpl in *; try congruence.
+      destruct (rs x0); try congruence.
+      assert (HB: (Int64.eq i i0) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto. }
+  (* Pbnel / Cmpl *)
+  { destruct optR0 as [[]|];
+    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+    unfold zero64, Op.zero64 in *;
+    eexists; eexists; eauto; split; constructor;
+    simpl in *; auto.
+    + destruct (rs x); simpl in *; try congruence.
+      assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto.
+    + destruct (rs x); simpl in *; try congruence.
+      assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto.
+    + destruct (rs x); simpl in *; try congruence.
+      destruct (rs x0); try congruence.
+      assert (HB: negb (Int64.eq i i0) = b) by congruence.
+      rewrite HB; destruct b; simpl; auto. }
+  (* Pbeql, Pbnel, Pbltl, Pbtlul, Pbgel, Pbgeul / Cmplu *)
+  1-6:
+    destruct optR0 as [[]|];
+    unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+    unfold zero64, Op.zero64 in *;
+    eexists; eexists; eauto; split; constructor;
+    simpl in *; try rewrite EVAL'; auto.
 Qed.
 
 Lemma transl_cbranch_correct_true:
@@ -647,405 +432,6 @@ Proof.
   intros; Simpl. 
 Qed.
 
-(** Translation of condition operators *)
-
-Lemma transl_cond_int32s_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m
-  /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool.
-  simpl. rewrite (Val.negate_cmp_bool Clt). 
-  destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt). 
-  destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_cond_int32u_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m
-  /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool.
-  simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle). 
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt). 
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_cond_int64s_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m
-  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool.
-  simpl. rewrite (Val.negate_cmpl_bool Clt). 
-  destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt). 
-  destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_cond_int64u_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m
-  /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2)
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool.
-  simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle). 
-  destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt). 
-  destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_condimm_int32s_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int32s.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C).
-  exists rs'; eauto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ unfold xorimm32. 
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ unfold xorimm32. 
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed).
-* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. 
-  unfold Int.lt. rewrite zlt_false. auto. 
-  change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed.
-  generalize (Int.signed_range i); omega.
-* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto.
-  unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
-  destruct (zlt (Int.signed n) (Int.signed i)).
-  rewrite zlt_false by omega. auto.
-  rewrite zlt_true by omega. auto.
-  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
-  assert (Int.signed n <> Int.max_signed).
-  { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. }
-  generalize (Int.signed_range n); omega.
-+ apply DFL.
-+ apply DFL.
-Qed.
-
-Lemma transl_condimm_int32u_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int32u.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split; auto. rewrite B; auto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ apply DFL.
-+ apply DFL.
-+ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto.
-  intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ apply DFL.
-+ apply DFL.
-+ apply DFL.
-Qed.
-
-Lemma transl_condimm_int64s_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int64s.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C).
-  exists rs'; eauto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ unfold xorimm64. 
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ unfold xorimm64. 
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed).
-* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. 
-  unfold Int64.lt. rewrite zlt_false. auto. 
-  change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed.
-  generalize (Int64.signed_range i); omega.
-* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto.
-  unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
-  destruct (zlt (Int64.signed n) (Int64.signed i)).
-  rewrite zlt_false by omega. auto.
-  rewrite zlt_true by omega. auto.
-  rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
-  assert (Int64.signed n <> Int64.max_signed).
-  { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
-  generalize (Int64.signed_range n); omega.
-+ apply DFL.
-+ apply DFL.
-Qed.
-
-Lemma transl_condimm_int64u_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int64u.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split; auto. rewrite B; auto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ apply DFL.
-+ apply DFL.
-+ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto.
-  intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ apply DFL.
-+ apply DFL.
-+ apply DFL.
-   Qed.
-
-Lemma transl_cond_op_correct:
-  forall cond rd args k c rs m,
-  transl_cond_op cond rd args k = OK c ->
-  exists rs',
-     exec_straight ge fn c rs m k rs' m
-  /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)).
-  { destruct ob as [[]|]; reflexivity. }
-  intros until m; intros TR.
-  destruct cond; simpl in TR; ArgsInv.
-+ (* cmp *)
-  exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
-+ (* cmpu *)
-  exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite B; auto.
-+ (* cmpimm *)
-  apply transl_condimm_int32s_correct; eauto with asmgen.
-+ (* cmpuimm *)
-  apply transl_condimm_int32u_correct; eauto with asmgen.
-+ (* cmpl *)
-  exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
-+ (* cmplu *)
-  exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C).
-   exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
-+ (* cmplimm *)
-  exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. 
-  intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
-+ (* cmpluimm *)
-  exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. 
-  intros (rs' & A & B & C).
-   exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
-+ (* cmpf *)
-  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
-  fold (Val.cmpf c0 (rs x) (rs x0)).
-  set (v := Val.cmpf c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
-  split; intros; Simpl.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_float_correct with (v := Val.notbool v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-+ (* notcmpf *)
-  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
-  rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)).
-  set (v := Val.cmpf c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_float_correct with (v := v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto.
-  split; intros; Simpl.
-+ (* cmpfs *)
-  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
-  fold (Val.cmpfs c0 (rs x) (rs x0)).
-  set (v := Val.cmpfs c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
-  split; intros; Simpl.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_single_correct with (v := Val.notbool v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-+ (* notcmpfs *)
-  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
-  rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)).
-  set (v := Val.cmpfs c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_single_correct with (v := v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
-  split; intros; Simpl.
-   Qed.
-
 (** Some arithmetic properties. *)
 
 Remark cast32unsigned_from_cast32signed:
@@ -1254,68 +640,22 @@ Opaque Int.eq.
       eapply exec_straight_step. simpl; reflexivity. auto. 
       apply exec_straight_one. simpl; reflexivity. auto. 
       split; intros; Simpl. }
-  (* cond *)
-  { 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:
     econstructor; split; try apply exec_straight_one; simpl; eauto;
     split; intros; Simpl; unfold may_undef_int; try destruct is_long; simpl;
     try rewrite Int.add_commut; try rewrite Int64.add_commut;
     destruct (rs (preg_of m0)); try discriminate; eauto.
-  all: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
-  econstructor; split; try apply exec_straight_one; simpl; eauto;
-  split; intros; Simpl.
-  all: destruct (rs x0); auto.
-  all: destruct (rs x1); auto.
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* shrxlimm *)
-  destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
-  {
-   exploit Val.shrxl_shrl_3; eauto. intros E; subst v.
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ destruct (Int.eq n Int.one).
-  * econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    apply exec_straight_one. simpl; reflexivity. auto.
-    split; intros; Simpl.
-
-  * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
-    econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    apply exec_straight_one. simpl; reflexivity. auto. 
-    split; intros; Simpl.
-  }
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ destruct (Int.eq n Int.one).
-  * econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    apply exec_straight_one. simpl; reflexivity. auto.
-    split; intros; Simpl.
-
-  * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
-    econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    apply exec_straight_one. simpl; reflexivity. auto. 
-    split; intros; Simpl.
-  
-- (* cond *)
-  exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. eauto with asmgen.
-- (* select *)
-  econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  1-12:
+    destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
+    econstructor; split; try apply exec_straight_one; simpl; eauto;
+    split; intros; Simpl;
+    destruct (rs x0); auto;
+    destruct (rs x1); auto.
+  (* select *)
+  { econstructor; split. apply exec_straight_one. simpl; eauto. auto.
   split; intros; Simpl.
-  apply Val.lessdef_normalize.
+  apply Val.lessdef_normalize. }
 Qed.
 
 (** Memory accesses *)
diff --git a/riscV/Op.v b/riscV/Op.v
index 4c2390a1..8b4d444d 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -200,8 +200,7 @@ Inductive operation : Type :=
   | OEfled                                       (**r compare less-than/equal *)
   | OEfeqs                                       (**r compare equal *)
   | OEflts                                       (**r compare less-than *)
-  | OEfles.                                      (**r compare less-than/equal *)
-  | Ocmp (cond: condition)  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | OEfles                                       (**r compare less-than/equal *)
   | Obits_of_single
   | Obits_of_float
   | Osingle_of_bits