diff options
| -rw-r--r-- | aarch64/Asmgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 5038245a..fcd12eef 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -223,7 +223,7 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction := do r1'' <- ireg_of_preg r1'; do r2'' <- ireg_of_preg r2'; OK (Asm.Pcsel rd' r1'' r2'' c) - | FR' r1', IR' r2' => do rd' <- freg_of_preg rd; + | FR' r1', FR' r2' => do rd' <- freg_of_preg rd; do r1'' <- freg_of_preg r1'; do r2'' <- freg_of_preg r2'; OK (Asm.Pfsel rd' r1'' r2'' c) |