From c764ff8433d8d4b31228d8313aa1043cb9196d21 Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Thu, 9 Jul 2020 08:32:36 +0200 Subject: Switch back to specific registers for specific (inlined) instruction --- aarch64/Asmblock.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 1abe7d90..5cabf324 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -445,7 +445,7 @@ Inductive ar_instruction : Type := (* PArithFR0 *) | Pfmovi (fsz : fsize) (rd : freg) (r1 : ireg0) (**r copy int reg to FP reg *) (* PArithCPPP *) - | Pcsel (rd r1 r2 : preg) (c : testcond) (**r int/float conditional move *) + | Pcsel (rd r1 r2 : ireg) (c : testcond) (**r int/float conditional move *) (* PArithAFFF *) | Pfnmul (fsz : fsize) (rd r1 r2 : freg) (**r multiply-negate *) . -- cgit