aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selection.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Selection.v')
-rw-r--r--backend/Selection.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/Selection.v b/backend/Selection.v
index edc63cd4..b35c891f 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -98,6 +98,8 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
| Cminor.Olonguoffloat => longuoffloat hf arg
| Cminor.Ofloatoflong => floatoflong hf arg
| Cminor.Ofloatoflongu => floatoflongu hf arg
+ | Cminor.Osingleoflong => singleoflong hf arg
+ | Cminor.Osingleoflongu => singleoflongu hf arg
end.
Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=