1 files changed, 7 insertions, 0 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index debe1928..b87d2692 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -722,6 +722,13 @@ Definition transl_op
       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.