diff --git a/CHANGELOG.md b/CHANGELOG.md
index d392df165c6d743c5284ffb2eb807c9871dca374..7747ffdaedb30b08d970e91af3b2dc9cc4bfbb9b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,6 +48,7 @@ Coq 8.13 is no longer supported.
   with list/maps of pairs; and `big_sepM <-> big_sepL` via `list_to_map` and
   `map_to_list`. (by Dorian Lesbre).
 - Make `persistently_True` a bi-entailment.
+- Make `BiLaterContractive` a class instead of a notation.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 2ff462f72be55a67cceee0b77ba4744f77e83424..5f82577225cd517363c991784a7cd64faa02041c 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -165,7 +165,7 @@ Global Instance uPred_pure_forall M : BiPureForall (uPredI M).
 Proof. exact: @pure_forall_2. Qed.
 
 Global Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
-Proof. apply later_contractive. Qed.
+Proof. exact: @later_contractive. Qed.
 
 Global Instance uPred_persistently_impl_plainly M : BiPersistentlyImplPlainly (uPredI M).
 Proof. exact: persistently_impl_plainly. Qed.
diff --git a/iris/bi/extensions.v b/iris/bi/extensions.v
index e54908d50287347146b9fd123c6c15842ce7eb90..f665cae03ed29b201a44e4103d49b251c2ef42fd 100644
--- a/iris/bi/extensions.v
+++ b/iris/bi/extensions.v
@@ -25,8 +25,8 @@ Class BiLöb (PROP : bi) :=
 Global Hint Mode BiLöb ! : typeclass_instances.
 Global Arguments löb_weak {_ _} _ _.
 
-Notation BiLaterContractive PROP :=
-  (Contractive (bi_later (PROP:=PROP))) (only parsing).
+Class BiLaterContractive (PROP : bi) :=
+  later_contractive :> Contractive (bi_later (PROP:=PROP)).
 
 (** The class [BiPersistentlyForall] states that universal quantification
 commutes with the persistently modality. The reverse direction of the entailment
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index fa923f412109cd974ea65c27f8fec1b94f07ae72..f5a8e0d07a69679bdc9f67047c826d6befed58b6 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -728,7 +728,7 @@ Section bi_facts.
 
   Global Instance monPred_later_contractive :
     BiLaterContractive PROP → BiLaterContractive monPredI.
-  Proof. unseal=> ? n P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
+  Proof. intros ? n. unseal=> P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
   Global Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
   Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
   Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index 9f3755aca05856a6aa0dba4f561a11eb0e390e1c..0b4d6389246d1dbf9876e3cf7c007862d872917b 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -125,7 +125,7 @@ Global Instance siProp_pure_forall : BiPureForall siPropI.
 Proof. exact: @pure_forall_2. Qed.
 
 Global Instance siProp_later_contractive : BiLaterContractive siPropI.
-Proof. apply later_contractive. Qed.
+Proof. exact: @later_contractive. Qed.
 
 Lemma siProp_internal_eq_mixin : BiInternalEqMixin siPropI (@siProp_internal_eq).
 Proof.