From aabfd379b2d58afc5b89dfa2d753e56354c1fccb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 29 Oct 2020 14:14:46 +0100 Subject: Bugfix in Asmgen --- aarch64/Asmgen.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/Asmgen.v') 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) -- cgit