1 files changed, 14 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index c03e319c..cf0b2a0a 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -729,6 +729,20 @@ Definition transl_op
       do rd <- ireg_of res;
       transl_cond_op cmp rd args k
 
+  | Oselect, a0 :: a1 :: aS :: nil =>
+    assertion (mreg_eq a0 res);
+      do r0 <- ireg_of a0;
+      do r1 <- ireg_of a1;
+      do rS <- ireg_of aS;
+        OK (Pcmove BTwnez r0 rS r1 ::i k)
+
+  | Oselectl, a0 :: a1 :: aS :: nil =>
+    assertion (mreg_eq a0 res);
+      do r0 <- ireg_of a0;
+      do r1 <- ireg_of a1;
+      do rS <- ireg_of aS;
+        OK (Pcmove BTdnez r0 rS r1 ::i k)
+
   | _, _ =>
       Error(msg "Asmgenblock.transl_op")
   end.