diff options
Diffstat (limited to 'kvx/Asmblockdeps.v')
| -rw-r--r-- | kvx/Asmblockdeps.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index a9786e0a..b1895ee6 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -1609,6 +1609,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pfminw => "Pfminw" | Pfmaxd => "Pfmaxd" | Pfmaxw => "Pfmaxw" + | Pabdw => "Pabdw" + | Pabdl => "Pabdl" end. Definition string_of_name_rri32 (n: arith_name_rri32): pstring := @@ -1636,6 +1638,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Psrlil => "Psrlil" | Psrail => "Psrail" | Psrxil => "Psrxil" + | Pabdiw => "Pabdiw" end. Definition string_of_name_rri64 (n: arith_name_rri64): pstring := @@ -1654,6 +1657,7 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := | Pnxoril => "Pnxoril" | Pandnil => "Pandnil" | Pornil => "Pornil" + | Pabdil => "Pabdil" end. Definition string_of_name_arrr (n: arith_name_arrr): pstring := |