From 2eb9e420ef5910e6b3be5735a7e38c86dcfdef36 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 29 May 2012 09:00:26 +0000
Subject: Removed Oandimm, etc, cases, because of 2-address constraints...

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1904 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 ia32/CombineOp.v | 15 ---------------
 1 file changed, 15 deletions(-)

(limited to 'ia32/CombineOp.v')

diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v
index 61f26e7..1391f55 100644
--- a/ia32/CombineOp.v
+++ b/ia32/CombineOp.v
@@ -68,21 +68,6 @@ Function combine_addr (addr: addressing) (args: list valnum) : option(addressing
 
 Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) :=
   match op, args with
-  | Oandimm n, x :: nil =>
-      match get x with
-      | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys)
-      | _ => None
-      end
-  | Oorimm n, x :: nil =>
-      match get x with
-      | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys)
-      | _ => None
-      end
-  | Oxorimm n, x :: nil =>
-      match get x with
-      | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys)
-      | _ => None
-      end
   | Olea addr, _ =>
       match combine_addr addr args with
       | Some(addr', args') => Some(Olea addr', args')
-- 
cgit v1.2.3