aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Op.v
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc/Op.v')
-rw-r--r--powerpc/Op.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 7ddbcc34..505b7545 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -573,8 +573,7 @@ Definition is_trapping_op (op : operation) :=
match op with
| Odiv | Odivl | Odivu | Odivlu
| Oshrximm _ | Oshrxlimm _
- | Ointoffloat | Ointuoffloat
- | Ofloatofint | Ofloatofintu
+ | Ointoffloat
| Olongoffloat
| Ofloatoflong => true
| _ => false