diff --git a/arm/SelectOp.v b/arm/SelectOp.v
index 8ac4ea5171ba2d763d7987e561ca896dc2c0c2a4..49676f839e00a07b175e4be83971aaa58838f9a0 100644
--- a/arm/SelectOp.v
+++ b/arm/SelectOp.v
@@ -1193,3 +1193,7 @@ Definition addressing (chunk: memory_chunk) (e: expr) :=
       (Aindexed Int.zero, e:::Enil)
   end.
 
+(** For compatibility with PowerPC, but unused. *)
+
+Parameter use_fused_mul : unit -> bool.
+