diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-07 09:46:13 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-07 09:46:13 +0200 |
| commit | 840899319d3a19269a6afe6f60e3a43d58647865 (patch) | |
| tree | 420e5550e232b1c18105d2eb2ac5c7e01908f5cb /aarch64/Asmblock.v | |
| parent | 1ddfc8323d64fb28fa1111b1cc630910cc2c27c3 (diff) | |
| download | compcert-kvx-840899319d3a19269a6afe6f60e3a43d58647865.tar.gz compcert-kvx-840899319d3a19269a6afe6f60e3a43d58647865.zip | |
Remove Pfsel which is currently identical to Pcsel
(since the grouping instructions by pregs)
Diffstat (limited to 'aarch64/Asmblock.v')
| -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 := |