aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selection.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Selection.v')
-rw-r--r--backend/Selection.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/Selection.v b/backend/Selection.v
index 23d8d22f..a55b1918 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -1095,6 +1095,7 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
| Cminor.Oabsf => Eop Oabsf (arg ::: Enil)
| Cminor.Osingleoffloat => singleoffloat arg
| Cminor.Ointoffloat => Eop Ointoffloat (arg ::: Enil)
+ | Cminor.Ointuoffloat => Eop Ointuoffloat (arg ::: Enil)
| Cminor.Ofloatofint => Eop Ofloatofint (arg ::: Enil)
| Cminor.Ofloatofintu => Eop Ofloatofintu (arg ::: Enil)
end.