diff options
| -rw-r--r-- | aarch64/Asmblock.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index a8157b17..b61288e9 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -388,9 +388,7 @@ Inductive arith_ppp : Type := Inductive arith_c_ppp : Type := (** Conditional data processing *) - | Pcsel (**r int conditional move *) - (** Floating-point conditional select *) - | Pfsel + | Pcsel (**r int/float conditional move *) . Inductive arith_rr0r : Type := |