aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Cminortyping.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Cminortyping.v')
-rw-r--r--backend/Cminortyping.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v
index 9f35fe35..d9e99122 100644
--- a/backend/Cminortyping.v
+++ b/backend/Cminortyping.v
@@ -64,6 +64,7 @@ Definition type_binop (op: binary_operation) : typ * typ * typ :=
| Ocmpf _ => (Tfloat, Tfloat, Tint)
| Ocmpfs _ => (Tsingle, Tsingle, Tint)
| Ocmpl _ | Ocmplu _ => (Tlong, Tlong, Tint)
+ | Oexpect ty => (ty, ty, ty)
end.
Module RTLtypes <: TYPE_ALGEBRA.