From 42d20911f3fa101219933667606c12076c0a6abc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 29 May 2019 10:31:22 +0200
Subject: [PATCH] experiment with restrict Hint Mode for Reflexive

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

diff --git a/theories/base.v b/theories/base.v
index 86d98c17..1d0ef607 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -39,6 +39,13 @@ Obligation Tactic := idtac.
 (** 3. Hide obligations from the results of the [Search] commands. *)
 Add Search Blacklist "_obligation_".
 
+(** Restrict Mode of some stdlib typeclasses. *)
+Hint Mode Reflexive ! ! : typeclass_instances.
+(* This needs a new instance to not break rewriting, see
+https://github.com/coq/coq/issues/7916. *)
+Instance: forall T (f : T -> Prop), Proper (eq ==> iff) f.
+Proof. now intros T f x y ->. Qed.
+
 (** * Sealing off definitions *)
 Section seal.
   Local Set Primitive Projections.
-- 
GitLab