diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-12-12 15:35:53 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-02-20 10:35:48 +0100 |
| commit | 668d546f670996d22e5d2a2f6f83752a8254dc23 (patch) | |
| tree | 7c334212b5da2456168ed636fc7e8cef4f8b9378 | |
| parent | e306714815c33121ee165b5e8825ca1c8187fc96 (diff) | |
| download | compcert-668d546f670996d22e5d2a2f6f83752a8254dc23.tar.gz compcert-668d546f670996d22e5d2a2f6f83752a8254dc23.zip | |
Remove unused definition
Closes: #467
| -rw-r--r-- | arm/Op.v | 4 |
1 files changed, 0 insertions, 4 deletions
@@ -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 := |