diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 313d54aa38e3e05c8d8281cd12f7ab063a8f70e0..0b728789cc87e1cce61bfd5851e570c653915767 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -78,7 +78,7 @@ Proof.
   intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
 Qed.
 Global Instance ownM_duplicable a : CoreId a → Duplicable (@uPred_ownM M a).
-Proof. intros. apply: persistent_sep_duplicable. Qed.
+Proof. intros. apply: persistent_duplicable. Qed.
 
 (** For big ops *)
 Global Instance uPred_ownM_sep_homomorphism :
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index c9f819ede0d737e4484f269e569ca07a310432f0..17051f58886df272003dddb901ec1b99ae5f2452 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1363,7 +1363,7 @@ Proof.
 Qed.
 
 (* Not an instance, see the bottom of this file *)
-Lemma persistent_sep_duplicable P
+Lemma persistent_duplicable P
   `{HP : !TCOr (Affine P) (Absorbing P), !Persistent P} :
   Duplicable P.
 Proof.
@@ -1581,7 +1581,7 @@ Lemma duplicable_and_persistent_r P Q :
 Proof. rewrite comm. apply duplicable_and_persistent_l. Qed.
 
 Global Instance persistently_duplicable P : Duplicable (<pers> P).
-Proof. apply: persistent_sep_duplicable. Qed.
+Proof. apply: persistent_duplicable. Qed.
 Global Instance absorbingly_duplicable P : Duplicable P → Duplicable (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 Global Instance absorbingly_if_duplicable p P : Duplicable P → Duplicable (<absorb>?p P).
@@ -1645,14 +1645,14 @@ Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → PROP)
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 End derived.
 
-(* When declared as an actual instance, [persistent_sep_duplicable] will cause
+(* When declared as an actual instance, [persistent_duplicable] will cause
 failing proof searches to take exponential time, as Coq will try to
 apply it the instance at any node in the proof search tree.
 
 To avoid that, we declare it using a [Hint Immediate], so that it will
 only be used at the leaves of the proof search tree, i.e. when the
 premise of the hint can be derived from just the current context. *)
-(* FIXME: This hint does not work due to the [TCOr] in [persistent_sep_duplicable]. *)
-Hint Immediate persistent_sep_duplicable : typeclass_instances.
+(* FIXME: This hint does not work due to the [TCOr] in [persistent_duplicable]. *)
+Hint Immediate persistent_duplicable : typeclass_instances.
 
 End bi.
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
index 736b6669fcf6631b8c2b54a3d000ccb8dc521679..e3f358374b24f1057bb4549ba802e9b620cfa016 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -221,7 +221,7 @@ Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
 Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
 Global Instance internal_eq_duplicable {A : ofeT} (a b : A) :
   Duplicable (PROP:=PROP) (a ≡ b).
-Proof. apply: persistent_sep_duplicable. Qed.
+Proof. apply: persistent_duplicable. Qed.
 
 (* Equality under a later. *)
 Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → PROP)
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index 6888a5f6a6cb261aaec514bc5109a2fafa60b99c..c91b638922f6adc9308b27e49ca60487fcfdca41 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -75,8 +75,8 @@ Section fractional.
   Global Instance persistent_fractional P :
     Persistent P → Absorbing P → Fractional (λ _, P).
   Proof.
-    (* FIXME: The hint for [persistent_sep_duplicable] should apply here. *)
-    intros ? ? q q'. apply: bi.duplicable_equiv. apply: bi.persistent_sep_duplicable.
+    (* FIXME: The hint for [persistent_duplicable] should apply here. *)
+    intros ? ? q q'. apply: bi.duplicable_equiv. apply: bi.persistent_duplicable.
   Qed.
   Global Instance duplicable_fractional P :
     Duplicable P → Absorbing P → Fractional (λ _, P).