1 files changed, 1 insertions, 9 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 57c49ef2..4e874ca8 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -1033,15 +1033,7 @@ Qed.
 Definition is_trapping_op (op : operation) :=
   match op with
   | Odiv | Odivl | Odivu | Odivlu
-  | Omod | Omodl | Omodu | Omodlu
-  | Oshrximm _ | Oshrxlimm _
-  | Ointoffloat | Ointuoffloat
-  | Ointofsingle | Ointuofsingle
-  | Olongoffloat | Olonguoffloat
-  | Olongofsingle | Olonguofsingle
-  | Osingleofint | Osingleofintu
-  | Osingleoflong | Osingleoflongu
-  | Ofloatoflong | Ofloatoflongu => true
+  | Omod | Omodl | Omodu | Omodlu => true
   | _ => false
   end.