aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblock.v
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/Asmblock.v')
-rw-r--r--aarch64/Asmblock.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index e362753b..ba6a64fa 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 : ireg) (c : testcond) (**r int/float conditional move *)
+ | Pcsel (rd r1 r2 : preg) (c : testcond) (**r int/float conditional move *)
(* PArithAFFF *)
| Pfnmul (fsz : fsize) (rd r1 r2 : freg) (**r multiply-negate *)
.