diff --git a/theories/base.v b/theories/base.v
index 86d98c17b6e8d2ac44d9ab595aeebbb89637c321..1d0ef607c027c27b907e6a3a5a66418af9cf2095 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.