diff --git a/_CoqProject b/_CoqProject
index cf13c3743775582b3232e6412a879e7c1f08fbf2..f7238a768c1d01a77f6d28dc89ecc2fa5a11f0d7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -20,8 +20,6 @@
 -arg -w -arg -future-coercion-class-field
 # Some warnings exist only on some Coq versions
 -arg -w -arg -unknown-warning
-# Since we still support Coq 8.15, we cannot yet deal with these deprecations.
--arg -w -arg -deprecated-since-8.18
 
 iris/prelude/options.v
 iris/prelude/prelude.v
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 82d6cf0796e48cb9a3905e986cd4a5ba5dc1bd5c..2c0a4098fd8c66bc316f2b3360650c49644ef4df 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1581,7 +1581,7 @@ Section iso_cofe_subtype.
   Context {A B : ofe} `{Cofe A} (P : A → Prop) (f : ∀ x, P x → B) (g : B → A).
   Context (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2).
   Let Hgne : NonExpansive g.
-  Proof. intros n y1 y2. apply g_dist. Qed.
+  Proof. intros n y1 y2. apply g_dist. Defined.
   Local Existing Instance Hgne.
   Context (gf : ∀ x Hx, g (f x Hx) ≡ x).
   Context (Hlimit : ∀ c : chain B, P (compl (chain_map g c))).
diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 5d7196da856379911205639f543fa459dbdf057c..d9bccd4ef1b876640185f8f058c1b8e06ab50891 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -149,14 +149,14 @@ induction principles:
 Section least_ind.
   Context {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
 
-  Let wf_pred_mono `{!NonExpansive Φ} :
+  Local Lemma Private_wf_pred_mono `{!NonExpansive Φ} :
     BiMonoPred (λ (Ψ : A → PROP) (a : A), Φ a ∧ F Ψ a)%I.
   Proof using Type*.
     split; last solve_proper.
     intros Ψ Ψ' Hne Hne'. iIntros "#Mon" (x) "Ha". iSplit; first by iDestruct "Ha" as "[$ _]".
     iDestruct "Ha" as "[_ Hr]". iApply (bi_mono_pred with "[] Hr"). by iModIntro.
   Qed.
-  Local Existing Instance wf_pred_mono.
+  Local Existing Instance Private_wf_pred_mono.
 
   Lemma least_fixpoint_ind_wf (Φ : A → PROP) `{!NonExpansive Φ} :
     □ (∀ y, F (bi_least_fixpoint (λ Ψ a, Φ a ∧ F Ψ a)) y -∗ Φ y) -∗
@@ -304,13 +304,14 @@ again. *)
 Section greatest_coind.
   Context {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
 
-  Let paco_mono `{!NonExpansive Φ} : BiMonoPred (λ (Ψ : A → PROP) (a : A), Φ a ∨ F Ψ a)%I.
+  Local Lemma Private_paco_mono `{!NonExpansive Φ} :
+    BiMonoPred (λ (Ψ : A → PROP) (a : A), Φ a ∨ F Ψ a)%I.
   Proof using Type*.
     split; last solve_proper.
     intros Ψ Ψ' Hne Hne'. iIntros "#Mon" (x) "[H1|H2]"; first by iLeft.
     iRight. iApply (bi_mono_pred with "[] H2"). by iModIntro.
   Qed.
-  Local Existing Instance paco_mono.
+  Local Existing Instance Private_paco_mono.
 
   Lemma greatest_fixpoint_paco (Φ : A → PROP) `{!NonExpansive Φ} :
     □ (∀ y, Φ y -∗ F (bi_greatest_fixpoint (λ Ψ a, Φ a ∨ F Ψ a)) y) -∗
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 2272e36eed5fd0244edaef65342110db98720364..956586906f448efea5aa41b32919c7ae371967cf 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -53,10 +53,10 @@ Section cofe.
       section by using Let. *)
     Let monPred_sig_equiv:
       ∀ P Q, P ≡ Q ↔ monPred_sig P ≡ monPred_sig Q.
-    Proof. by split; [intros []|]. Qed.
+    Proof. by split; [intros []|]. Defined.
     Let monPred_sig_dist:
       ∀ n, ∀ P Q : monPred, P ≡{n}≡ Q ↔ monPred_sig P ≡{n}≡ monPred_sig Q.
-    Proof. by split; [intros []|]. Qed.
+    Proof. by split; [intros []|]. Defined.
 
     Definition monPred_ofe_mixin : OfeMixin monPred.
     Proof.