aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--aarch64/Op.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/aarch64/Op.v b/aarch64/Op.v
index 30f806d3..ef28dd6d 100644
--- a/aarch64/Op.v
+++ b/aarch64/Op.v
@@ -926,8 +926,6 @@ Qed.
Definition is_trapping_op (op : operation) :=
match op with
- | Odiv | Odivu | Odivl | Odivlu
- | Oshrximm _ | Oshrlximm _
| Ointoffloat | Ointuoffloat
| Ointofsingle | Ointuofsingle
| Ofloatofint | Ofloatofintu