1 files changed, 0 insertions, 4 deletions
diff --git a/arm/Op.v b/arm/Op.v
index 4739ef2e..375a626d 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -671,10 +671,6 @@ Proof.
   destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. do 4 f_equal. symmetry; auto with ptrofs.
 Qed.
 
-(** Two-address operations.  There are none in the ARM architecture. *)
-
-Definition two_address_op (op: operation) : bool := false.
-
 (** Operations that are so cheap to recompute that CSE should not factor them out. *)
 
 Definition is_trivial_op (op: operation) : bool :=