diff options
| -rw-r--r-- | mppa_k1c/Asmblock.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index fdec8ed2..ac4b7951 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -370,6 +370,9 @@ Inductive arith_name_rrr : Type := | Pfsbfw (**r float sub word *) | Pfmuld (**r float multiply double *) | Pfmulw (**r float multiply word *) +(* + | Pcmove (it: itest) (**r conditional move *) + *) . Inductive arith_name_rri32 : Type := |