From 668d546f670996d22e5d2a2f6f83752a8254dc23 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 12 Dec 2022 15:35:53 +0100 Subject: Remove unused definition Closes: #467 --- arm/Op.v | 4 ---- 1 file changed, 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 := -- cgit