From 62316a8e94d8cdcbf9e7aeadd1caf8e29507e6b0 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 24 Feb 2012 16:43:38 +0000
Subject: Take advantage of Cmaskzero and Cmasknotzero.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1825 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/SelectOp.vp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'arm/SelectOp.vp')

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 7b8851c9..27b5f536 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -454,4 +454,4 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | _ => (Aindexed Int.zero, e:::Enil)
   end.
 
-
+Definition cond_of_expr (e: expr) := (Ccompuimm Cne Int.zero, e:::Enil).
-- 
cgit