diff --git a/theories/base.v b/theories/base.v
index df49b47de9e9bb1c89b34669386330bcefcffbb2..2de465415f7044997542dfa86a622dde134417ca 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.