experiment with restrict Hint Mode for Reflexive

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.