aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/Asmvliw.v
diff options
context:
space:
mode:
Diffstat (limited to 'kvx/Asmvliw.v')
-rw-r--r--kvx/Asmvliw.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v
index bbd40692..0ce2ed69 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -1087,7 +1087,7 @@ Definition arith_eval_rri64 n v i :=
| Pornil => Val.orl (Val.notl v) (Vlong i)
| Paddxil shift => ExtValues.addxl (int_of_shift1_4 shift) v (Vlong i)
| Prevsubxil shift => ExtValues.revsubxl (int_of_shift1_4 shift) v (Vlong i)
- | Pabdil => ExtValues.absdiff v (Vlong i)
+ | Pabdil => ExtValues.absdiffl v (Vlong i)
end.
Definition cmove bt v1 v2 v3 :=