diff --git a/theories/base.v b/theories/base.v
index f5a415ea145977d0630d11f0b8d950592d597e46..8b7a1218882e577a4d6e5b6c5b83cabf2633f12d 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -772,6 +772,8 @@ End prod_relation.
 Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) :=
   prod_relation (≡) (≡).
 
+(** Below we make [prod_equiv] type class opaque, so we first lift all
+instances *)
 Section prod_setoid.
   Context `{Equiv A, Equiv B}.