From 29af30c29fd808840f2d7e58b9cec24d3f658b56 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 6 Jun 2021 14:08:56 +0200
Subject: [PATCH] update 'Equiv' mode comment

---
 theories/base.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index df49b47d..2de46541 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -247,8 +247,7 @@ Proof. split; repeat intro; congruence. Qed.
 "canonical" equivalence for a type. The typeclass is tied to the \equiv
 symbol. This is based on (Spitters/van der Weegen, 2011). *)
 Class Equiv A := equiv: relation A.
-(* No Hint Mode set because of Coq bugs #5735 and #9058, only
-fixed in Coq >= 8.12.
+(* No Hint Mode set because of Coq bug #14441.
 Global Hint Mode Equiv ! : typeclass_instances. *)
 
 Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
-- 
GitLab