Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp

1 files changed, 4 insertions, 4 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 4f9d008b..8b86ec5a 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -812,10 +812,10 @@ Definition transl_op
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Pxoriw rd rs n :: k)
-  | OEluiw n _, a1 :: nil =>
+  | OEluiw n, nil =>
       do rd <- ireg_of res;
       OK (Pluiw rd n :: k)
-  | OEaddiwr0 n _, a1 :: nil =>
+  | OEaddiwr0 n, nil =>
       do rd <- ireg_of res;
       OK (Paddiw rd X0 n :: k)
   | OEseql optR0, a1 :: a2 :: nil =>
@@ -860,10 +860,10 @@ Definition transl_op
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Pxoril rd rs n :: k)
-  | OEluil n, a1 :: nil =>
+  | OEluil n, nil =>
       do rd <- ireg_of res;
       OK (Pluil rd n :: k)
-  | OEaddilr0 n, a1 :: nil =>
+  | OEaddilr0 n, nil =>
       do rd <- ireg_of res;
       OK (Paddil rd X0 n :: k)
   | OEloadli n, nil =>