summaryrefslogtreecommitdiff
path: root/ia32/SelectOp.v
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/SelectOp.v')
-rw-r--r--ia32/SelectOp.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/ia32/SelectOp.v b/ia32/SelectOp.v
index 4a4d9e1..c1f5703 100644
--- a/ia32/SelectOp.v
+++ b/ia32/SelectOp.v
@@ -61,7 +61,7 @@ Definition addrstack (ofs: int) :=
(** ** Boolean negation *)
Definition notbool_base (e: expr) :=
- Eop (Ocmp (Ccompimm Ceq Int.zero)) (e ::: Enil).
+ Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil).
Fixpoint notbool (e: expr) {struct e} : expr :=
match e with