Merge of branch seq-and-or. See Changelog for details.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

12 files changed, 114 insertions, 521 deletions

diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index 780d812..fba85ff 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -35,13 +35,11 @@ rule token = parse
   | "/*"         { comment lexbuf; token lexbuf }
   | "absf" { ABSF }
   | "&" { AMPERSAND }
-  | "&&" { AMPERSANDAMPERSAND }
   | "!"    { BANG }
   | "!="    { BANGEQUAL }
   | "!=f"    { BANGEQUALF }
   | "!=u"    { BANGEQUALU }
   | "|"     { BAR }
-  | "||"    { BARBAR }
   | "^"     { CARET }
   | "case"  { CASE }
   | ":"    { COLON }
@@ -102,7 +100,6 @@ rule token = parse
   | "%u"    { PERCENTU }
   | "+"    { PLUS }
   | "+f"    { PLUSF }
-  | "?"    { QUESTION }
   | "}"    { RBRACE }
   | "}}"    { RBRACERBRACE }
   | "]"    { RBRACKET }
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 4a91a01..aec0a5e 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -34,7 +34,6 @@ type rexpr =
   | Runop of unary_operation * rexpr
   | Rbinop of binary_operation * rexpr * rexpr
   | Rload of memory_chunk * rexpr
-  | Rcondition of rexpr * rexpr * rexpr
   | Rcall of signature * rexpr * rexpr list
 
 let temp_counter = ref 0
@@ -59,11 +58,6 @@ let rec convert_rexpr = function
       let c2 = convert_rexpr e2 in
       Ebinop(op, c1, c2)
   | Rload(chunk, e1) -> Eload(chunk, convert_rexpr e1)
-  | Rcondition(e1, e2, e3) ->
-      let c1 = convert_rexpr e1 in
-      let c2 = convert_rexpr e2 in
-      let c3 = convert_rexpr e3 in
-      Econdition(c1, c2, c3)
   | Rcall(sg, e1, el) ->
       let c1 = convert_rexpr e1 in
       let cl = convert_rexpr_list el in
@@ -135,11 +129,6 @@ let mkwhile expr body =
 let intconst n =
   Rconst(Ointconst(coqint_of_camlint n))
 
-let andbool e1 e2 =
-  Rcondition(e1, e2, intconst 0l)
-let orbool e1 e2 =
-  Rcondition(e1, intconst 1l, e2)
-
 let exitnum n = nat_of_camlint n
 
 let mkswitch expr (cases, dfl) =
@@ -202,13 +191,11 @@ let mkmatch expr cases =
 
 %token ABSF
 %token AMPERSAND
-%token AMPERSANDAMPERSAND
 %token BANG
 %token BANGEQUAL
 %token BANGEQUALF
 %token BANGEQUALU
 %token BAR
-%token BARBAR
 %token CARET
 %token CASE
 %token COLON
@@ -273,7 +260,6 @@ let mkmatch expr cases =
 %token PERCENTU
 %token PLUS
 %token PLUSF
-%token QUESTION
 %token RBRACE
 %token RBRACERBRACE
 %token RBRACKET
@@ -301,9 +287,6 @@ let mkmatch expr cases =
 %left COMMA
 %left p_let
 %right EQUAL
-%right QUESTION COLON
-%left BARBAR
-%left AMPERSANDAMPERSAND
 %left BAR
 %left CARET
 %left AMPERSAND
@@ -502,7 +485,7 @@ expr:
   | FLOATOFINT expr                             { Runop(Ofloatofint, $2) }
   | FLOATOFINTU expr                            { Runop(Ofloatofintu, $2) }
   | TILDE expr                                  { Runop(Onotint, $2) }
-  | BANG expr                                   { Runop(Onotbool, $2) }
+  | BANG expr                                   { Rbinop(Ocmpu Ceq, $2, intconst 0l) }
   | INT8S expr                                  { Runop(Ocast8signed, $2) }
   | INT8U expr                                  { Runop(Ocast8unsigned, $2) }
   | INT16S expr                                 { Runop(Ocast16signed, $2) }
@@ -544,9 +527,6 @@ expr:
   | expr GREATERF expr                          { Rbinop(Ocmpf Cgt, $1, $3) }
   | expr GREATEREQUALF expr                     { Rbinop(Ocmpf Cge, $1, $3) }
   | memory_chunk LBRACKET expr RBRACKET         { Rload($1, $3) }
-  | expr AMPERSANDAMPERSAND expr                { andbool $1 $3 }
-  | expr BARBAR expr                            { orbool $1 $3 }
-  | expr QUESTION expr COLON expr               { Rcondition($1, $3, $5) }
   | expr LPAREN expr_list RPAREN COLON signature{ Rcall($6, $1, $3) }
 ;
 
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 6e91f5b..4070785 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -90,8 +90,6 @@ let type_unary_operation = function
   | Ocast8unsigned -> tint, tint
   | Ocast16unsigned -> tint, tint
   | Onegint -> tint, tint
-  | Oboolval -> tint, tint
-  | Onotbool -> tint, tint
   | Onotint -> tint, tint
   | Onegf -> tfloat, tfloat
   | Oabsf -> tfloat, tfloat
@@ -135,8 +133,6 @@ let name_of_unary_operation = function
   | Ocast8unsigned -> "cast8unsigned"
   | Ocast16unsigned -> "cast16unsigned"
   | Onegint -> "negint"
-  | Oboolval -> "notbool"
-  | Onotbool -> "notbool"
   | Onotint -> "notint"
   | Onegf -> "negf"
   | Oabsf -> "absf"
@@ -224,24 +220,6 @@ let rec type_expr env lenv e =
                               (name_of_chunk chunk) s))
       end;
       type_chunk chunk
-  | Econdition(e1, e2, e3) ->
-      type_condexpr env lenv e1;
-      let te2 = type_expr env lenv e2 in
-      let te3 = type_expr env lenv e3 in
-      begin try
-        unify te2 te3
-      with Error s ->
-        raise (Error (sprintf "In conditional expression:\n%s" s))
-      end;
-      te2
-(*
-  | Elet(e1, e2) ->
-      let te1 = type_expr env lenv e1 in
-      let te2 = type_expr env (te1 :: lenv) e2 in
-      te2
-  | Eletvar n ->
-      type_letvar lenv n
-*)
 
 and type_exprlist env lenv el =
   match el with
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 6d288a9..4bc6b72 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -44,9 +44,7 @@ Inductive unary_operation : Type :=
   | Ocast8signed: unary_operation          (**r 8-bit sign extension  *)
   | Ocast16unsigned: unary_operation       (**r 16-bit zero extension  *)
   | Ocast16signed: unary_operation         (**r 16-bit sign extension *)
-  | Oboolval: unary_operation              (**r 0 if null, 1 if non-null *)
   | Onegint: unary_operation               (**r integer opposite *)
-  | Onotbool: unary_operation              (**r boolean negation  *)
   | Onotint: unary_operation               (**r bitwise complement  *)
   | Onegf: unary_operation                 (**r float opposite *)
   | Oabsf: unary_operation                 (**r float absolute value *)
@@ -87,8 +85,7 @@ Inductive expr : Type :=
   | Econst : constant -> expr
   | Eunop : unary_operation -> expr -> expr
   | Ebinop : binary_operation -> expr -> expr -> expr
-  | Eload : memory_chunk -> expr -> expr
-  | Econdition : expr -> expr -> expr -> expr.
+  | Eload : memory_chunk -> expr -> expr.
 
 (** Statements include expression evaluation, assignment to local variables,
   memory stores, function calls, an if/then/else conditional, infinite
@@ -230,9 +227,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   | Ocast8signed => Some (Val.sign_ext 8 arg)
   | Ocast16unsigned => Some (Val.zero_ext 16 arg)
   | Ocast16signed => Some (Val.sign_ext 16 arg)
-  | Oboolval => Some(Val.boolval arg)
   | Onegint => Some (Val.negint arg)
-  | Onotbool => Some (Val.notbool arg)
   | Onotint => Some (Val.notint arg)
   | Onegf => Some (Val.negf arg)
   | Oabsf => Some (Val.absf arg)
@@ -301,12 +296,7 @@ Inductive eval_expr: expr -> val -> Prop :=
   | eval_Eload: forall chunk addr vaddr v,
       eval_expr addr vaddr ->
       Mem.loadv chunk m vaddr = Some v ->     
-      eval_expr (Eload chunk addr) v
-  | eval_Econdition: forall a1 a2 a3 v1 b1 v2,
-      eval_expr a1 v1 ->
-      Val.bool_of_val v1 b1 ->
-      eval_expr (if b1 then a2 else a3) v2 ->
-      eval_expr (Econdition a1 a2 a3) v2.
+      eval_expr (Eload chunk addr) v.
 
 Inductive eval_exprlist: list expr -> list val -> Prop :=
   | eval_Enil:
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index a8e49e8..bb5143c 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -35,34 +35,26 @@ Require Import Smallstep.
   languages ([RTL] and below).  Moreover, to express sharing of
   sub-computations, a "let" binding is provided (constructions
   [Elet] and [Eletvar]), using de Bruijn indices to refer to "let"-bound
-  variables.  Finally, a variant [condexpr] of [expr]
-  is used to represent expressions which are evaluated for their
-  boolean value only and not their exact value.
-*)
+  variables. *)
 
 Inductive expr : Type :=
   | Evar : ident -> expr
   | Eop : operation -> exprlist -> expr
   | Eload : memory_chunk -> addressing -> exprlist -> expr
-  | Econdition : condexpr -> expr -> expr -> expr
+  | Econdition : condition -> exprlist -> expr -> expr -> expr
   | Elet : expr -> expr -> expr
   | Eletvar : nat -> expr
 
-with condexpr : Type :=
-  | CEtrue: condexpr
-  | CEfalse: condexpr
-  | CEcond: condition -> exprlist -> condexpr
-  | CEcondition : condexpr -> condexpr -> condexpr -> condexpr
-
 with exprlist : Type :=
   | Enil: exprlist
   | Econs: expr -> exprlist -> exprlist.
 
 Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope.
 
-(** Statements are as in Cminor, except that the condition of an
-  if/then/else conditional is a [condexpr], and the [Sstore] construct
-  uses a machine-dependent addressing mode. *)
+(** Statements are as in Cminor, except that the [Sifthenelse]
+  construct uses a machine-dependent condition (with multiple
+  arguments), and the [Sstore] construct uses a machine-dependent
+  addressing mode. *)
 
 Inductive stmt : Type :=
   | Sskip: stmt
@@ -72,7 +64,7 @@ Inductive stmt : Type :=
   | Stailcall: signature -> expr + ident -> exprlist -> stmt
   | Sbuiltin : option ident -> external_function -> exprlist -> stmt
   | Sseq: stmt -> stmt -> stmt
-  | Sifthenelse: condexpr -> stmt -> stmt -> stmt
+  | Sifthenelse: condition -> exprlist -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
   | Sblock: stmt -> stmt
   | Sexit: nat -> stmt
@@ -147,10 +139,7 @@ Variable ge: genv.
 
 (** The evaluation predicates have the same general shape as those
     of Cminor.  Refer to the description of Cminor semantics for
-    the meaning of the parameters of the predicates.
-    One additional predicate is introduced:
-    [eval_condexpr ge sp e m le a b], meaning that the conditional
-    expression [a] evaluates to the boolean [b]. *)
+    the meaning of the parameters of the predicates. *)
 
 Section EVAL_EXPR.
 
@@ -171,10 +160,11 @@ Inductive eval_expr: letenv -> expr -> val -> Prop :=
       eval_addressing ge sp addr vl = Some vaddr ->
       Mem.loadv chunk m vaddr = Some v ->     
       eval_expr le (Eload chunk addr al) v
-  | eval_Econdition: forall le a b c v1 v2,
-      eval_condexpr le a v1 ->
-      eval_expr le (if v1 then b else c) v2 ->
-      eval_expr le (Econdition a b c) v2
+  | eval_Econdition: forall le cond al b c vl vb v,
+      eval_exprlist le al vl ->
+      eval_condition cond vl m = Some vb ->
+      eval_expr le (if vb then b else c) v ->
+      eval_expr le (Econdition cond al b c) v
   | eval_Elet: forall le a b v1 v2,
       eval_expr le a v1 ->
       eval_expr (v1 :: le) b v2 ->
@@ -183,20 +173,6 @@ Inductive eval_expr: letenv -> expr -> val -> Prop :=
       nth_error le n = Some v ->
       eval_expr le (Eletvar n) v
 
-with eval_condexpr: letenv -> condexpr -> bool -> Prop :=
-  | eval_CEtrue: forall le,
-      eval_condexpr le CEtrue true
-  | eval_CEfalse: forall le,
-      eval_condexpr le CEfalse false
-  | eval_CEcond: forall le cond al vl b,
-      eval_exprlist le al vl ->
-      eval_condition cond vl m = Some b ->
-      eval_condexpr le (CEcond cond al) b
-  | eval_CEcondition: forall le a b c vb1 vb2,
-      eval_condexpr le a vb1 ->
-      eval_condexpr le (if vb1 then b else c) vb2 ->
-      eval_condexpr le (CEcondition a b c) vb2
-
 with eval_exprlist: letenv -> exprlist -> list val -> Prop :=
   | eval_Enil: forall le,
       eval_exprlist le Enil nil
@@ -204,9 +180,8 @@ with eval_exprlist: letenv -> exprlist -> list val -> Prop :=
       eval_expr le a1 v1 -> eval_exprlist le al vl ->
       eval_exprlist le (Econs a1 al) (v1 :: vl).
 
-Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop
-  with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop
-  with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop.
+Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop
+  with eval_exprlist_ind2 := Minimality for eval_exprlist Sort Prop.
 
 Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop :=
   | eval_eos_e: forall le e v,
@@ -245,7 +220,7 @@ Fixpoint find_label (lbl: label) (s: stmt) (k: cont)
       | Some sk => Some sk
       | None => find_label lbl s2 k
       end
-  | Sifthenelse a s1 s2 =>
+  | Sifthenelse cond al s1 s2 =>
       match find_label lbl s1 k with
       | Some sk => Some sk
       | None => find_label lbl s2 k
@@ -316,9 +291,10 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sseq s1 s2) k sp e m)
         E0 (State f s1 (Kseq s2 k) sp e m)
 
-  | step_ifthenelse: forall f a s1 s2 k sp e m b,
-      eval_condexpr sp e m nil a b ->
-      step (State f (Sifthenelse a s1 s2) k sp e m)
+  | step_ifthenelse: forall f cond al s1 s2 k sp e m vl b,
+      eval_exprlist sp e m nil al vl ->
+      eval_condition cond vl m = Some b ->
+      step (State f (Sifthenelse cond al s1 s2) k sp e m)
         E0 (State f (if b then s1 else s2) k sp e m)
 
   | step_loop: forall f s k sp e m,
@@ -395,7 +371,7 @@ Inductive final_state: state -> int -> Prop :=
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
-Hint Constructors eval_expr eval_condexpr eval_exprlist: evalexpr.
+Hint Constructors eval_expr eval_exprlist: evalexpr.
 
 (** * Lifting of let-bound variables *)
 
@@ -409,22 +385,13 @@ Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr :=
   | Evar id => Evar id
   | Eop op bl => Eop op (lift_exprlist p bl)
   | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl)
-  | Econdition b c d =>
-      Econdition (lift_condexpr p b) (lift_expr p c) (lift_expr p d)
+  | Econdition cond al b c =>
+      Econdition cond (lift_exprlist p al) (lift_expr p b) (lift_expr p c)
   | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c)
   | Eletvar n =>
       if le_gt_dec p n then Eletvar (S n) else Eletvar n
   end
 
-with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr :=
-  match a with
-  | CEtrue => CEtrue
-  | CEfalse => CEfalse
-  | CEcond cond bl => CEcond cond (lift_exprlist p bl)
-  | CEcondition b c d =>
-      CEcondition (lift_condexpr p b) (lift_condexpr p c) (lift_condexpr p d)
-  end
-
 with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist :=
   match a with
   | Enil => Enil
@@ -478,29 +445,22 @@ Lemma eval_lift_expr:
   eval_expr ge sp e m le' (lift_expr p a) v.
 Proof.
   intros until w.
-  apply (eval_expr_ind3 ge sp e m
+  apply (eval_expr_ind2 ge sp e m
     (fun le a v =>
       forall p le', insert_lenv le p w le' ->
       eval_expr ge sp e m le' (lift_expr p a) v)
-    (fun le a v =>
-      forall p le', insert_lenv le p w le' ->
-      eval_condexpr ge sp e m le' (lift_condexpr p a) v)
     (fun le al vl =>
       forall p le', insert_lenv le p w le' ->
       eval_exprlist ge sp e m le' (lift_exprlist p al) vl));
   simpl; intros; eauto with evalexpr.
 
-  destruct v1; eapply eval_Econdition;
-  eauto with evalexpr; simpl; eauto with evalexpr.
+  eapply eval_Econdition; eauto. destruct vb; eauto.
 
   eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto.
 
   case (le_gt_dec p n); intro. 
   apply eval_Eletvar. eapply insert_lenv_lookup2; eauto.
   apply eval_Eletvar. eapply insert_lenv_lookup1; eauto.
-
-  destruct vb1; eapply eval_CEcondition;
-  eauto with evalexpr; simpl; eauto with evalexpr.
 Qed.
 
 Lemma eval_lift:
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 66b579e..858ef21 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -40,7 +40,6 @@ let rec precedence = function
   | Ebinop(Oxor, _, _) -> (7, LtoR)
   | Ebinop(Oor, _, _) -> (6, LtoR)
   | Eload _ -> (15, RtoL)
-  | Econdition _ -> (3, RtoL)
 
 (* Naming idents.  We assume idents are encoded as in Cminorgen. *)
 
@@ -58,8 +57,6 @@ let name_of_unop = function
   | Ocast16unsigned -> "int16u"
   | Ocast16signed -> "int16s"
   | Onegint -> "-"
-  | Oboolval -> "(_Bool)"
-  | Onotbool -> "!"
   | Onotint -> "~"
   | Onegf -> "-f"
   | Oabsf -> "absf"
@@ -141,8 +138,6 @@ let rec expr p (prec, e) =
                  expr (prec1, a1) (name_of_binop op) expr (prec2, a2)
   | Eload(chunk, a1) ->
       fprintf p "%s[%a]" (name_of_chunk chunk) expr (0, a1)
-  | Econdition(a1, a2, a3) ->
-      fprintf p "%a@ ? %a@ : %a" expr (4, a1) expr (4, a2) expr (4, a3)
   end;
   if prec' < prec then fprintf p ")@]" else fprintf p "@]"
 
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 86c1177..d3b99bb 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -416,10 +416,12 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
       do rl <- alloc_regs map al;
       do no <- add_instr (Iload chunk addr rl rd nd);
          transl_exprlist map al rl no
-  | Econdition b c d =>
-      do nfalse <- transl_expr map d rd nd;
-      do ntrue  <- transl_expr map c rd nd;
-         transl_condition map b ntrue nfalse
+  | Econdition cond al b c =>
+      do rl <- alloc_regs map al;
+      do nfalse <- transl_expr map c rd nd;
+      do ntrue  <- transl_expr map b rd nd;
+      do nt <- add_instr (Icond cond rl ntrue nfalse);
+         transl_exprlist map al rl nt
   | Elet b c =>
       do r  <- new_reg;
       do nc <- transl_expr (add_letvar map r) c rd nd;
@@ -428,28 +430,6 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
       do r <- find_letvar map n; add_move r rd nd
   end
 
-(** Translation of a conditional expression.  Similar to [transl_expr],
-  but the expression is evaluated for its truth value, and the generated
-  code branches to one of two possible continuation nodes [ntrue] or 
-  [nfalse] depending on the truth value of [a]. *)
-
-with transl_condition (map: mapping) (a: condexpr) (ntrue nfalse: node)
-                      {struct a}: mon node :=
-  match a with
-  | CEtrue =>
-      ret ntrue
-  | CEfalse =>
-      ret nfalse
-  | CEcond cond bl =>
-      do rl <- alloc_regs map bl;
-      do nt <- add_instr (Icond cond rl ntrue nfalse);
-         transl_exprlist map bl rl nt
-  | CEcondition b c d =>
-      do nd <- transl_condition map d ntrue nfalse;
-      do nc <- transl_condition map c ntrue nfalse;
-         transl_condition map b nc nd
-  end
-
 (** Translation of a list of expressions.  The expressions are evaluated
   left-to-right, and their values stored in the given list of registers. *)
 
@@ -472,7 +452,7 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node)
   no impact on program correctness.  We delegate the choice to an
   external heuristic (written in OCaml), declared below.  *)
 
-Parameter more_likely: condexpr -> stmt -> stmt -> bool.
+Parameter more_likely: condition -> stmt -> stmt -> bool.
 
 (** Auxiliary for translating [Sswitch] statements. *)
 
@@ -521,7 +501,7 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
 Fixpoint expr_is_2addr_op (e: expr) : bool :=
   match e with
   | Eop op _ => two_address_op op
-  | Econdition e1 e2 e3 => expr_is_2addr_op e2 || expr_is_2addr_op e3
+  | Econdition cond el e2 e3 => expr_is_2addr_op e2 || expr_is_2addr_op e3
   | Elet e1 e2 => expr_is_2addr_op e2
   | _ => false
   end.
@@ -587,15 +567,18 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
   | Sseq s1 s2 =>
       do ns <- transl_stmt map s2 nd nexits ngoto nret rret;
       transl_stmt map s1 ns nexits ngoto nret rret
-  | Sifthenelse a strue sfalse =>
-      if more_likely a strue sfalse then
+  | Sifthenelse cond al strue sfalse =>
+      do rl <- alloc_regs map al;
+      if more_likely cond strue sfalse then
         do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret;
         do ntrue  <- transl_stmt map strue  nd nexits ngoto nret rret;
-        transl_condition map a ntrue nfalse
+        do nt <- add_instr (Icond cond rl ntrue nfalse);
+           transl_exprlist map al rl nt
       else
         do ntrue  <- transl_stmt map strue  nd nexits ngoto nret rret;
         do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret;
-        transl_condition map a ntrue nfalse
+        do nt <- add_instr (Icond cond rl ntrue nfalse);
+           transl_exprlist map al rl nt
   | Sloop sbody =>
       do n1 <- reserve_instr;
       do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret;
@@ -650,7 +633,7 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state)
                         {struct s} : labelmap * state :=
   match s with
   | Sseq s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
-  | Sifthenelse c s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
+  | Sifthenelse cond al s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
   | Sloop s1 => reserve_labels s1 ms
   | Sblock s1 => reserve_labels s1 ms
   | Slabel lbl s1 => alloc_label lbl (reserve_labels s1 ms)
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index 0822587..245b80c 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -14,7 +14,7 @@ open Camlcoq
 open Switch
 open CminorSel
 
-let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = false
+let more_likely (c: Op.condition) (ifso: stmt) (ifnot: stmt) = false
 
 module IntOrd =
   struct
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index e06224a..659e8d0 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -520,9 +520,6 @@ Definition transl_expr_prop
   /\ rs'#rd = v
   /\ (forall r, In r pr -> rs'#r = rs#r).
 
-(** The simulation properties for lists of expressions and for
-  conditional expressions are similar. *)
-
 Definition transl_exprlist_prop 
      (le: letenv) (al: exprlist) (vl: list val) : Prop :=
   forall cs f map pr ns nd rl rs
@@ -535,18 +532,6 @@ Definition transl_exprlist_prop
   /\ rs'##rl = vl
   /\ (forall r, In r pr -> rs'#r = rs#r).
 
-Definition transl_condition_prop 
-     (le: letenv) (a: condexpr) (vb: bool) : Prop :=
-  forall cs f map pr ns ntrue nfalse rs
-    (MWF: map_wf map)
-    (TE: tr_condition f.(fn_code) map pr a ns ntrue nfalse)
-    (ME: match_env map e le rs),
-  exists rs',
-     star step tge (State cs f sp ns rs m) E0
-                   (State cs f sp (if vb then ntrue else nfalse) rs' m)
-  /\ match_env map e le rs'
-  /\ (forall r, In r pr -> rs'#r = rs#r).
-
 (** The correctness of the translation is a huge induction over
   the Cminor evaluation derivation for the source program.  To keep
   the proof manageable, we put each case of the proof in a separate
@@ -632,22 +617,25 @@ Proof.
 Qed.
 
 Lemma transl_expr_Econdition_correct:
-  forall (le : letenv) (cond : condexpr) (ifso ifnot : expr)
-         (vcond : bool) (v : val),
-  eval_condexpr ge sp e m le cond vcond ->
-  transl_condition_prop le cond vcond ->
+  forall (le : letenv) (cond : condition) (al: exprlist) (ifso ifnot : expr)
+         (vl: list val) (vcond : bool) (v : val),
+  eval_exprlist ge sp e m le al vl ->
+  transl_exprlist_prop le al vl ->
+  eval_condition cond vl m = Some vcond ->
   eval_expr ge sp e m le (if vcond then ifso else ifnot) v ->
   transl_expr_prop le (if vcond then ifso else ifnot) v ->
-  transl_expr_prop le (Econdition cond ifso ifnot) v.
+  transl_expr_prop le (Econdition cond al ifso ifnot) v.
 Proof.
-  intros; red; intros; inv TE. 
-  exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]].
+  intros; red; intros; inv TE. inv H14.
+  exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. 
   assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd dst).
     destruct vcond; auto.
-  exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
+  exploit H3; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
   exists rs2.
 (* Exec *)
-  split. eapply star_trans. eexact EX1. eexact EX2. auto. 
+  split. eapply star_trans. eexact EX1.
+  eapply star_left. eapply exec_Icond. eauto. rewrite RES1; eauto. reflexivity. 
+  eexact EX2. reflexivity. traceEq.
 (* Match-env *)
   split. assumption.
 (* Result value *)
@@ -710,67 +698,6 @@ Proof.
   apply OTHER1. intuition congruence.
 Qed.
 
-Lemma transl_condition_CEtrue_correct:
-  forall (le : letenv),
-  transl_condition_prop le CEtrue true.
-Proof.
-  intros; red; intros; inv TE. 
-  exists rs. split. apply star_refl. split. auto. auto.
-Qed.    
-
-Lemma transl_condition_CEfalse_correct:
-  forall (le : letenv),
-  transl_condition_prop le CEfalse false.
-Proof.
-  intros; red; intros; inv TE. 
-  exists rs. split. apply star_refl. split. auto. auto.
-Qed.    
-
-Lemma transl_condition_CEcond_correct:
-  forall (le : letenv) (cond : condition) (args : exprlist)
-         (vargs : list val) (b : bool),
-  eval_exprlist ge sp e m le args vargs ->
-  transl_exprlist_prop le args vargs ->
-  eval_condition cond vargs m = Some b ->
-  transl_condition_prop le (CEcond cond args) b.
-Proof.
-  intros; red; intros; inv TE.
-  exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  exists rs1.
-(* Exec *)
-  split. eapply star_right. eexact EX1. 
-  eapply exec_Icond with (b := b); eauto. 
-  rewrite RES1. auto.
-  traceEq.
-(* Match-env *)
-  split. assumption.
-(* Regs *)
-  auto.
-Qed.
-
-Lemma transl_condition_CEcondition_correct:
-  forall (le : letenv) (cond ifso ifnot : condexpr) (vcond v : bool),
-  eval_condexpr ge sp e m le cond vcond ->
-  transl_condition_prop le cond vcond ->
-  eval_condexpr ge sp e m le (if vcond then ifso else ifnot) v ->
-  transl_condition_prop le (if vcond then ifso else ifnot) v ->
-  transl_condition_prop le (CEcondition cond ifso ifnot) v.
-Proof.
-  intros; red; intros; inv TE. 
-  exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]].
-  assert (tr_condition f.(fn_code) map pr (if vcond then ifso else ifnot)
-             (if vcond then ntrue' else nfalse') ntrue nfalse).
-    destruct vcond; auto.
-  exploit H2; eauto. intros [rs2 [EX2 [ME2 OTHER2]]].
-  exists rs2.
-(* Execution *)
-  split. eapply star_trans. eexact EX1. eexact EX2. auto. 
-(* Match-env *)
-  split. auto.
-(* Regs *)
-  intros. transitivity (rs1#r); auto.
-Qed.
- 
 Lemma transl_exprlist_Enil_correct:
   forall (le : letenv),
   transl_exprlist_prop le Enil nil.
@@ -814,31 +741,8 @@ Theorem transl_expr_correct:
   eval_expr ge sp e m le a v ->
   transl_expr_prop le a v.
 Proof
-  (eval_expr_ind3 ge sp e m
-     transl_expr_prop
-     transl_condition_prop
-     transl_exprlist_prop
-     transl_expr_Evar_correct
-     transl_expr_Eop_correct
-     transl_expr_Eload_correct
-     transl_expr_Econdition_correct
-     transl_expr_Elet_correct
-     transl_expr_Eletvar_correct
-     transl_condition_CEtrue_correct
-     transl_condition_CEfalse_correct
-     transl_condition_CEcond_correct
-     transl_condition_CEcondition_correct
-     transl_exprlist_Enil_correct
-     transl_exprlist_Econs_correct).
-
-Theorem transl_condexpr_correct:
-  forall le a v,
-  eval_condexpr ge sp e m le a v ->
-  transl_condition_prop le a v.
-Proof
-  (eval_condexpr_ind3 ge sp e m
+  (eval_expr_ind2 ge sp e m
      transl_expr_prop
-     transl_condition_prop
      transl_exprlist_prop
      transl_expr_Evar_correct
      transl_expr_Eop_correct
@@ -846,22 +750,16 @@ Proof
      transl_expr_Econdition_correct
      transl_expr_Elet_correct
      transl_expr_Eletvar_correct
-     transl_condition_CEtrue_correct
-     transl_condition_CEfalse_correct
-     transl_condition_CEcond_correct
-     transl_condition_CEcondition_correct
      transl_exprlist_Enil_correct
      transl_exprlist_Econs_correct).
 
-
 Theorem transl_exprlist_correct:
   forall le a v,
   eval_exprlist ge sp e m le a v ->
   transl_exprlist_prop le a v.
 Proof
-  (eval_exprlist_ind3 ge sp e m
+  (eval_exprlist_ind2 ge sp e m
      transl_expr_prop
-     transl_condition_prop
      transl_exprlist_prop
      transl_expr_Evar_correct
      transl_expr_Eop_correct
@@ -869,10 +767,6 @@ Proof
      transl_expr_Econdition_correct
      transl_expr_Elet_correct
      transl_expr_Eletvar_correct
-     transl_condition_CEtrue_correct
-     transl_condition_CEfalse_correct
-     transl_condition_CEcond_correct
-     transl_condition_CEcondition_correct
      transl_exprlist_Enil_correct
      transl_exprlist_Econs_correct).
 
@@ -886,7 +780,7 @@ Fixpoint size_stmt (s: stmt) : nat :=
   match s with
   | Sskip => 0
   | Sseq s1 s2 => (size_stmt s1 + size_stmt s2 + 1)
-  | Sifthenelse e s1 s2 => (size_stmt s1 + size_stmt s2 + 1)
+  | Sifthenelse cond el s1 s2 => (size_stmt s1 + size_stmt s2 + 1)
   | Sloop s1 => (size_stmt s1 + 1)
   | Sblock s1 => (size_stmt s1 + 1)
   | Sexit n => 0
@@ -1219,11 +1113,10 @@ Proof.
   econstructor; eauto. econstructor; eauto. 
 
   (* ifthenelse *)
-  inv TS.
-  exploit transl_condexpr_correct; eauto. 
-  intros [rs' [A [B C]]].
+  inv TS. inv H13.
+  exploit transl_exprlist_correct; eauto. intros [rs' [A [B [C D]]]].
   econstructor; split.
-  right; split. eexact A. destruct b; Lt_state.
+  left. eapply plus_right. eexact A. eapply exec_Icond; eauto. rewrite C; eauto. traceEq.
   destruct b; econstructor; eauto. 
 
   (* loop *)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index f6c59fc..579a6c2 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -749,11 +749,11 @@ Inductive tr_expr (c: code):
       c!n1 = Some (Iload chunk addr rl rd nd) ->
       reg_map_ok map rd dst -> ~In rd pr ->
       tr_expr c map pr (Eload chunk addr al) ns nd rd dst
-  | tr_Econdition: forall map pr b ifso ifnot ns nd rd ntrue nfalse dst,
-      tr_condition c map pr b ns ntrue nfalse ->
+  | tr_Econdition: forall map pr cond bl ifso ifnot ns nd rd ntrue nfalse dst,
+      tr_condition c map pr cond bl ns ntrue nfalse ->
       tr_expr c map pr ifso ntrue nd rd dst ->
       tr_expr c map pr ifnot nfalse nd rd dst ->
-      tr_expr c map pr (Econdition b ifso ifnot) ns nd rd dst
+      tr_expr c map pr (Econdition cond bl ifso ifnot) ns nd rd dst
   | tr_Elet: forall map pr b1 b2 ns nd rd n1 r dst,
       ~reg_in_map map r ->
       tr_expr c map pr b1 ns n1 r None ->
@@ -765,26 +765,17 @@ Inductive tr_expr (c: code):
       tr_move c ns r nd rd ->
       tr_expr c map pr (Eletvar n) ns nd rd dst
 
-(** [tr_condition c map pr cond ns ntrue nfalse rd] holds if the graph [c],
+(** [tr_condition c map pr cond al ns ntrue nfalse rd] holds if the graph [c],
   starting at node [ns], contains instructions that compute the truth
   value of the Cminor conditional expression [cond] and terminate
   on node [ntrue] if the condition holds and on node [nfalse] otherwise. *)
 
 with tr_condition (c: code): 
-       mapping -> list reg -> condexpr -> node -> node -> node -> Prop :=
-  | tr_CEtrue: forall map pr ntrue nfalse,
-      tr_condition c map pr CEtrue ntrue ntrue nfalse
-  | tr_CEfalse: forall map pr ntrue nfalse,
-      tr_condition c map pr CEfalse nfalse ntrue nfalse
+       mapping -> list reg -> condition -> exprlist -> node -> node -> node -> Prop :=
   | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl,
       tr_exprlist c map pr bl ns n1 rl ->
       c!n1 = Some (Icond cond rl ntrue nfalse) ->
-      tr_condition c map pr (CEcond cond bl) ns ntrue nfalse
-  | tr_CEcondition: forall map pr b ifso ifnot ns ntrue nfalse ntrue' nfalse',
-      tr_condition c map pr b ns ntrue' nfalse' ->
-      tr_condition c map pr ifso ntrue' ntrue nfalse ->
-      tr_condition c map pr ifnot nfalse' ntrue nfalse ->
-      tr_condition c map pr (CEcondition b ifso ifnot) ns ntrue nfalse
+      tr_condition c map pr cond bl ns ntrue nfalse
 
 (** [tr_exprlist c map pr exprs ns nd rds] holds if the graph [c],
   between nodes [ns] and [nd], contains instructions that compute the values
@@ -889,11 +880,11 @@ Inductive tr_stmt (c: code) (map: mapping):
      tr_stmt c map s2 n nd nexits ngoto nret rret ->
      tr_stmt c map s1 ns n nexits ngoto nret rret ->
      tr_stmt c map (Sseq s1 s2) ns nd nexits ngoto nret rret
-  | tr_Sifthenelse: forall a strue sfalse ns nd nexits ngoto nret rret ntrue nfalse,
+  | tr_Sifthenelse: forall cond al strue sfalse ns nd nexits ngoto nret rret ntrue nfalse,
      tr_stmt c map strue ntrue nd nexits ngoto nret rret ->
      tr_stmt c map sfalse nfalse nd nexits ngoto nret rret ->
-     tr_condition c map nil a ns ntrue nfalse ->
-     tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret
+     tr_condition c map nil cond al ns ntrue nfalse ->
+     tr_stmt c map (Sifthenelse cond al strue sfalse) ns nd nexits ngoto nret rret
   | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop nend,
      tr_stmt c map sbody nloop nend nexits ngoto nret rret ->
      c!ns = Some(Inop nloop) ->
@@ -963,9 +954,9 @@ Lemma tr_expr_incr:
   tr_expr s2.(st_code) map pr a ns nd rd dst
 with tr_condition_incr:
   forall s1 s2, state_incr s1 s2 ->
-  forall map pr a ns ntrue nfalse,
-  tr_condition s1.(st_code) map pr a ns ntrue nfalse ->
-  tr_condition s2.(st_code) map pr a ns ntrue nfalse
+  forall map pr cond al ns ntrue nfalse,
+  tr_condition s1.(st_code) map pr cond al ns ntrue nfalse ->
+  tr_condition s2.(st_code) map pr cond al ns ntrue nfalse
 with tr_exprlist_incr:
   forall s1 s2, state_incr s1 s2 ->
   forall map pr al ns nd rl,
@@ -1004,13 +995,6 @@ Lemma transl_expr_charact:
      (VALID2: reg_valid rd s),
    tr_expr s'.(st_code) map pr a ns nd rd None
 
-with transl_condexpr_charact:
-  forall a map ntrue nfalse s ns s' pr INCR
-     (TR: transl_condition map a ntrue nfalse s = OK ns s' INCR)
-     (VALID: regs_valid pr s)
-     (WF: map_valid map s),
-   tr_condition s'.(st_code) map pr a ns ntrue nfalse
-
 with transl_exprlist_charact:
   forall al map rl nd s ns s' pr INCR
      (TR: transl_exprlist map al rl nd s = OK ns s' INCR)
@@ -1040,9 +1024,10 @@ Proof.
   (* Econdition *)
   inv OK.
   econstructor; eauto with rtlg.
-  apply tr_expr_incr with s1; auto. 
+  econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. 
+  apply tr_expr_incr with s2; auto. 
   eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto.
-  apply tr_expr_incr with s0; auto. 
+  apply tr_expr_incr with s1; auto. 
   eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto.
   (* Elet *)
   inv OK.
@@ -1065,24 +1050,6 @@ Proof.
   eapply add_move_charact; eauto.
   monadInv EQ1.
 
-(* Conditions *)
-  induction a; intros; try (monadInv TR); saturateTrans.
-
-  (* CEtrue *)
-  constructor.
-  (* CEfalse *)
-  constructor.
-  (* CEcond *)
-  econstructor; eauto with rtlg.
-  eapply transl_exprlist_charact; eauto with rtlg.
-  (* CEcondition *)
-  econstructor.
-  eapply transl_condexpr_charact; eauto with rtlg.
-  apply tr_condition_incr with s1; auto.
-  eapply transl_condexpr_charact; eauto with rtlg.
-  apply tr_condition_incr with s0; auto.
-  eapply transl_condexpr_charact; eauto with rtlg.
-
 (* Lists *)
 
   induction al; intros; try (monadInv TR); saturateTrans.
@@ -1127,10 +1094,10 @@ Opaque two_address_op.
   (* Econdition *)
   simpl in NOT2ADDR. destruct (orb_false_elim _ _ NOT2ADDR).
   econstructor; eauto with rtlg.
-  eapply transl_condexpr_charact; eauto with rtlg.
+  econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. 
+  apply tr_expr_incr with s2; auto. 
+  eapply IHa1; eauto 2 with rtlg. 
   apply tr_expr_incr with s1; auto. 
-  eapply IHa1; eauto 2 with rtlg.
-  apply tr_expr_incr with s0; auto. 
   eapply IHa2; eauto 2 with rtlg.
   (* Elet *)
   simpl in NOT2ADDR.
@@ -1298,19 +1265,21 @@ Proof.
   eapply IHstmt2; eauto with rtlg.
   eapply IHstmt1; eauto with rtlg.
   (* Sifthenelse *)
-  destruct (more_likely c stmt1 stmt2); monadInv TR.
+  destruct (more_likely c stmt1 stmt2); monadInv EQ0.
   econstructor.
-  apply tr_stmt_incr with s1; auto. 
+  apply tr_stmt_incr with s2; auto. 
   eapply IHstmt1; eauto with rtlg.
-  apply tr_stmt_incr with s0; auto.
+  apply tr_stmt_incr with s1; auto.
   eapply IHstmt2; eauto with rtlg.
-  eapply transl_condexpr_charact; eauto with rtlg.
+  econstructor; eauto with rtlg. 
+  eapply transl_exprlist_charact; eauto with rtlg.
   econstructor.
-  apply tr_stmt_incr with s0; auto. 
+  apply tr_stmt_incr with s1; auto. 
   eapply IHstmt1; eauto with rtlg.
-  apply tr_stmt_incr with s1; auto.
+  apply tr_stmt_incr with s2; auto.
   eapply IHstmt2; eauto with rtlg.
-  eapply transl_condexpr_charact; eauto with rtlg.
+  econstructor; eauto with rtlg. 
+  eapply transl_exprlist_charact; eauto with rtlg.
   (* Sloop *)
   econstructor. 
   apply tr_stmt_incr with s1; auto. 
diff --git a/backend/Selection.v b/backend/Selection.v
index 11654f1..ff4d863 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -37,51 +37,12 @@ Require Import SelectOp.
 
 Open Local Scope cminorsel_scope.
 
-(** Conversion of conditional expressions *)
+(** Conversion of conditions *)
 
-Fixpoint negate_condexpr (e: condexpr): condexpr :=
+Function condition_of_expr (e: expr) : condition * exprlist :=
   match e with
-  | CEtrue => CEfalse
-  | CEfalse => CEtrue
-  | CEcond c el => CEcond (negate_condition c) el
-  | CEcondition e1 e2 e3 =>
-      CEcondition e1 (negate_condexpr e2) (negate_condexpr e3)
-  end.
-
-Definition is_compare_neq_zero (c: condition) : bool :=
-  match c with
-  | Ccompimm Cne n => Int.eq n Int.zero
-  | Ccompuimm Cne n => Int.eq n Int.zero
-  | _ => false
-  end.
-
-Definition is_compare_eq_zero (c: condition) : bool :=
-  match c with
-  | Ccompimm Ceq n => Int.eq n Int.zero
-  | Ccompuimm Ceq n => Int.eq n Int.zero
-  | _ => false
-  end.
-
-Definition condexpr_of_expr_base (e: expr) : condexpr :=
-  let (c, args) := cond_of_expr e in CEcond c args.
-
-Fixpoint condexpr_of_expr (e: expr) : condexpr :=
-  match e with
-  | Eop (Ointconst n) Enil =>
-      if Int.eq n Int.zero then CEfalse else CEtrue
-  | Eop (Ocmp c) (e1 ::: Enil) =>
-      if is_compare_neq_zero c then
-        condexpr_of_expr e1
-      else if is_compare_eq_zero c then
-        negate_condexpr (condexpr_of_expr e1)
-      else
-        CEcond c (e1 ::: Enil)
-  | Eop (Ocmp c) el =>
-      CEcond c el
-  | Econdition ce e1 e2 =>
-      CEcondition ce (condexpr_of_expr e1) (condexpr_of_expr e2)
-  | _ =>
-      condexpr_of_expr_base e
+  | Eop (Ocmp c) el => (c, el)
+  | _ => (Ccompuimm Cne Int.zero, e ::: Enil)
   end.
 
 (** Conversion of loads and stores *)
@@ -115,8 +76,6 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Ocast16unsigned => cast16unsigned arg 
   | Cminor.Ocast16signed => cast16signed arg 
   | Cminor.Onegint => negint arg
-  | Cminor.Oboolval => boolval arg
-  | Cminor.Onotbool => notbool arg
   | Cminor.Onotint => notint arg
   | Cminor.Onegf => negf arg
   | Cminor.Oabsf => absf arg
@@ -160,9 +119,6 @@ Fixpoint sel_expr (a: Cminor.expr) : expr :=
   | Cminor.Eunop op arg => sel_unop op (sel_expr arg)
   | Cminor.Ebinop op arg1 arg2 => sel_binop op (sel_expr arg1) (sel_expr arg2)
   | Cminor.Eload chunk addr => load chunk (sel_expr addr)
-  | Cminor.Econdition cond ifso ifnot =>
-      Econdition (condexpr_of_expr (sel_expr cond))
-                 (sel_expr ifso) (sel_expr ifnot)
   end.
 
 Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist :=
@@ -222,8 +178,8 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt :=
       end
   | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2)
   | Cminor.Sifthenelse e ifso ifnot =>
-      Sifthenelse (condexpr_of_expr (sel_expr e))
-                  (sel_stmt ge ifso) (sel_stmt ge ifnot)
+      let (cond, args) := condition_of_expr (sel_expr e) in
+      Sifthenelse cond args (sel_stmt ge ifso) (sel_stmt ge ifnot)
   | Cminor.Sloop body => Sloop (sel_stmt ge body)
   | Cminor.Sblock body => Sblock (sel_stmt ge body)
   | Cminor.Sexit n => Sexit n
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 79c039f..2fb56f8 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -40,125 +40,23 @@ Variable sp: val.
 Variable e: env.
 Variable m: mem.
 
-(** Conversion of condition expressions. *)
-
-Lemma negate_condexpr_correct:
-  forall le a b,
-  eval_condexpr ge sp e m le a b ->
-  eval_condexpr ge sp e m le (negate_condexpr a) (negb b).
-Proof.
-  induction 1; simpl.
-  constructor.
-  constructor.
-  econstructor. eauto. rewrite eval_negate_condition. rewrite H0. auto.
-  econstructor. eauto. destruct vb1; auto.
-Qed. 
-
-Scheme expr_ind2 := Induction for expr Sort Prop
-  with exprlist_ind2 := Induction for exprlist Sort Prop.
-
-Fixpoint forall_exprlist (P: expr -> Prop) (el: exprlist) {struct el}: Prop :=
-  match el with
-  | Enil => True
-  | Econs e el' => P e /\ forall_exprlist P el'
-  end.
-
-Lemma expr_induction_principle:
-  forall (P: expr -> Prop),
-  (forall i : ident, P (Evar i)) ->
-  (forall (o : operation) (e : exprlist),
-     forall_exprlist P e -> P (Eop o e)) ->
-  (forall (m : memory_chunk) (a : Op.addressing) (e : exprlist),
-     forall_exprlist P e -> P (Eload m a e)) ->
-  (forall (c : condexpr) (e : expr),
-     P e -> forall e0 : expr, P e0 -> P (Econdition c e e0)) ->
-  (forall e : expr, P e -> forall e0 : expr, P e0 -> P (Elet e e0)) ->
-  (forall n : nat, P (Eletvar n)) ->
-  forall e : expr, P e.
-Proof.
-  intros. apply expr_ind2 with (P := P) (P0 := forall_exprlist P); auto.
-  simpl. auto.
-  intros. simpl. auto.
-Qed.
-
-Lemma eval_condition_of_expr_base:
-  forall le a v b,
-  eval_expr ge sp e m le a v ->
-  Val.bool_of_val v b ->
-  eval_condexpr ge sp e m le (condexpr_of_expr_base a) b.
-Proof.
-  intros. unfold condexpr_of_expr_base.
-  generalize (eval_cond_of_expr _ _ _ _ _ _ _ _ H H0). 
-  destruct (cond_of_expr a) as [cond args]. 
-  intros [vl [A B]].
-  econstructor; eauto. 
-Qed.
-
-Lemma is_compare_neq_zero_correct:
-  forall c v b,
-  is_compare_neq_zero c = true ->
-  eval_condition c (v :: nil) m = Some b ->
-  Val.bool_of_val v b.
-Proof.
-  intros.
-  destruct c; simpl in H; try discriminate;
-  destruct c; simpl in H; try discriminate;
-  generalize (Int.eq_spec i Int.zero); rewrite H; intros; subst.
-
-  simpl in H0. destruct v; inv H0. constructor. 
-  simpl in H0. destruct v; inv H0. constructor. constructor.
-Qed.
-
-Lemma is_compare_eq_zero_correct:
-  forall c v b,
-  is_compare_eq_zero c = true ->
-  eval_condition c (v :: nil) m = Some b ->
-  Val.bool_of_val v (negb b).
-Proof.
-  intros. apply is_compare_neq_zero_correct with (negate_condition c).
-  destruct c; simpl in H; simpl; try discriminate;
-  destruct c; simpl; try discriminate; auto.
-  rewrite eval_negate_condition. rewrite H0. auto.
-Qed.
-
 Lemma eval_condition_of_expr:
-  forall a le v b,
+  forall le a v b,
   eval_expr ge sp e m le a v ->
   Val.bool_of_val v b ->
-  eval_condexpr ge sp e m le (condexpr_of_expr a) b.
+  match condition_of_expr a with (cond, args) =>
+    exists vl,
+    eval_exprlist ge sp e m le args vl /\
+    eval_condition cond vl m = Some b
+  end.
 Proof.
-  intro a0; pattern a0.
-  apply expr_induction_principle; simpl; intros;
-    try (eapply eval_condition_of_expr_base; eauto; fail).
-  
-  destruct o; try (eapply eval_condition_of_expr_base; eauto; fail).
-
-  destruct e0. inv H0. inv H5. simpl in H7. inv H7. inv H1.
-  destruct (Int.eq i Int.zero); constructor.
-  eapply eval_condition_of_expr_base; eauto.
-
-  inv H0. simpl in H7.
-  assert (eval_condition c vl m = Some b).
-    inv H7. eapply Val.bool_of_val_of_optbool; eauto.
-  assert (eval_condexpr ge sp e m le (CEcond c e0) b).
-    eapply eval_CEcond; eauto.
-  destruct e0; auto. destruct e1; auto.
-  simpl in H. destruct H.
-  inv H5. inv H11.
-
-  case_eq (is_compare_neq_zero c); intros.
-  eapply H; eauto.
-  apply is_compare_neq_zero_correct with c; auto.
-
-  case_eq (is_compare_eq_zero c); intros.
-  replace b with (negb (negb b)). apply negate_condexpr_correct.
-  eapply H; eauto.
-  apply is_compare_eq_zero_correct with c; auto.
-  apply negb_involutive.
-
-  auto.
-
-  inv H1. destruct v1; eauto with evalexpr.
+  intros until a. functional induction (condition_of_expr a); intros.
+(* compare *)
+  inv H. exists vl; split; auto.
+  simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto.
+(* default *)
+  exists (v :: nil); split. constructor. auto. constructor.
+  simpl. inv H0. auto. auto. 
 Qed.
 
 Lemma eval_load:
@@ -202,9 +100,7 @@ Proof.
   apply eval_cast8signed; auto.
   apply eval_cast16unsigned; auto.
   apply eval_cast16signed; auto.
-  apply eval_boolval; auto.
   apply eval_negint; auto.
-  apply eval_notbool; auto.
   apply eval_notint; auto.
   apply eval_negf; auto.
   apply eval_absf; auto.
@@ -436,14 +332,6 @@ Proof.
   exploit IHeval_expr; eauto. intros [vaddr' [A B]].
   exploit Mem.loadv_extends; eauto. intros [v' [C D]].
   exists v'; split; auto. eapply eval_load; eauto.
-  (* Econdition *)
-  exploit IHeval_expr1; eauto. intros [v1' [A B]].
-  exploit IHeval_expr2; eauto. intros [v2' [C D]].
-  replace (sel_expr (if b1 then a2 else a3)) with (if b1 then sel_expr a2 else sel_expr a3) in C.
-  assert (Val.bool_of_val v1' b1). inv B. auto. inv H0.
-  exists v2'; split; auto. 
-  econstructor; eauto. eapply eval_condition_of_expr; eauto. 
-  destruct b1; auto.
 Qed.
 
 Lemma sel_exprlist_correct:
@@ -544,6 +432,7 @@ Proof.
   destruct (find_label lbl (sel_stmt ge s1) (Kseq (sel_stmt ge s2) k')) as [[sy ky] | ];
   intuition. apply IHs2; auto.
 (* ifthenelse *)
+  destruct (condition_of_expr (sel_expr e)) as [cond args]. simpl.
   exploit (IHs1 k); eauto. 
   destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ];
   destruct (find_label lbl (sel_stmt ge s1) k') as [[sy ky] | ];
@@ -643,8 +532,11 @@ Proof.
   (* Sifthenelse *)
   exploit sel_expr_correct; eauto. intros [v' [A B]].
   assert (Val.bool_of_val v' b). inv B. auto. inv H0.
+  exploit eval_condition_of_expr; eauto.
+  destruct (condition_of_expr (sel_expr a)) as [cond args].
+  intros [vl' [C D]].
   left; exists (State (sel_function ge f) (if b then sel_stmt ge s1 else sel_stmt ge s2) k' sp e' m'); split.
-  constructor. eapply eval_condition_of_expr; eauto.
+  econstructor; eauto. 
   constructor; auto. destruct b; auto.
   (* Sloop *)
   left; econstructor; split. constructor. constructor; auto. constructor; auto.