diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index 9f04dd7ed0a566d6939218422f4a68bdbed025df..8d9110eff060555e812daefbe878030a313d0b69 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -413,7 +413,11 @@ Section homomorphisms.
Context `{Monoid M1 o1, Monoid M2 o2}.
Infix "`o1`" := o1 (at level 50, left associativity).
Infix "`o2`" := o2 (at level 50, left associativity).
- Instance foo {A} (R : relation A) : RewriteRelation R.
+ (** The ssreflect rewrite tactic only works for relations that have a
+ [RewriteRelation] instance. For the purpose of this section, we want to
+ rewrite with arbitrary relations, so we declare any relation to be a
+ [RewriteRelation]. *)
+ Local Instance: ∀ {A} (R : relation A), RewriteRelation R.
Lemma big_opL_commute {A} (h : M1 → M2) `{!MonoidHomomorphism o1 o2 R h}
(f : nat → A → M1) l :