From 45eca3da2b60d77c2549ac4debb753d96e45d067 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Nov 2020 13:19:55 +0100
Subject: [PATCH] rename persistent_sep_duplicable -> persistent_duplicable

---
 theories/base_logic/derived.v |  2 +-
 theories/bi/derived_laws.v    | 10 +++++-----
 theories/bi/internal_eq.v     |  2 +-
 theories/bi/lib/fractional.v  |  4 ++--
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 313d54aa3..0b728789c 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 c9f819ede..17051f588 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 736b6669f..e3f358374 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 6888a5f6a..c91b63892 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).
-- 
GitLab