From cb9cef38d26990a02c9804a8791e92240b0d22c1 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 11 Apr 2021 16:56:37 +0000
Subject: [PATCH] Hint Mode Equiv: update link to blocking Coq issue

Based on
https://github.com/coq/coq/issues/9058#issuecomment-496479506.
---
 theories/base.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index 8f31d3e6..309a844f 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -226,7 +226,8 @@ 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 bug #5735
+(* No Hint Mode set because of Coq bugs #5735 and #9058, only
+fixed in Coq >= 8.12.
 Global Hint Mode Equiv ! : typeclass_instances. *)
 
 Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
-- 
GitLab