From 1ef8320959bb3c872806b99f269cba5cea6094fd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Jul 2021 18:53:08 +0200
Subject: [PATCH] Comment.

---
 theories/base.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index f5a415ea..8b7a1218 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}.
 
-- 
GitLab