summaryrefslogtreecommitdiff
path: root/arm/Op.v
diff options
context:
space:
mode:
Diffstat (limited to 'arm/Op.v')
-rw-r--r--arm/Op.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/arm/Op.v b/arm/Op.v
index 5e85aae..1f26a72 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -79,7 +79,7 @@ Inductive operation : Type :=
| Osub: operation (**r [rd = r1 - r2] *)
| Osubshift: shift -> operation (**r [rd = r1 - shifted r2] *)
| Orsubshift: shift -> operation (**r [rd = shifted r2 - r1] *)
- | Orsubimm: int -> operation (**r [rd = r1 - n] *)
+ | Orsubimm: int -> operation (**r [rd = n - r1] *)
| Omul: operation (**r [rd = r1 * r2] *)
| Odiv: operation (**r [rd = r1 / r2] (signed) *)
| Odivu: operation (**r [rd = r1 / r2] (unsigned) *)