From 5347b5d5a87dbd09bc5081663bdd438ee67a6c5f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Oct 2023 10:26:37 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20instances=20`union=5Fwith=5Fproper`=20?=
 =?UTF-8?q?=E2=86=92=20`union=5Fwith=5Fne`,=20`map=5Ffmap=5Fproper`=20?=
 =?UTF-8?q?=E2=86=92=20`map=5Ffmap=5Fne`,=20`map=5Fzip=5Fwith=5Fproper`=20?=
 =?UTF-8?q?=E2=86=92=20`map=5Fzip=5Fwith=5Fne`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md        | 2 ++
 iris/algebra/gmap.v | 6 +++---
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7a82ef0c7..fc8d8565a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -53,6 +53,8 @@ Coq 8.13, 8.14, and 8.15 are no longer supported.
 * Add monotone resource algebra, `algebra/mra.v`, to enable reasoning about
   monotonicity with respect to an arbitrary preorder relation: the extension order
   of `mra R` is designed to embed the preorder relation `R`. (by Amin Timany)
+* Rename instances `union_with_proper` → `union_with_ne`,
+  `map_fmap_proper` → `map_fmap_ne`, `map_zip_with_proper` → `map_zip_with_ne`.
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index fed922c7f..41542e659 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -118,17 +118,17 @@ Proof.
   intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
   destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
 Qed.
-Global Instance union_with_proper `{Countable K} {A : ofe} n :
+Global Instance union_with_ne `{Countable K} {A : ofe} n :
   Proper ((dist n ==> dist n ==> dist n) ==>
           dist n ==> dist n ==> dist n) (union_with (M:=gmap K A)).
 Proof.
   intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
   by do 2 destruct 1; first [apply Hf | constructor].
 Qed.
-Global Instance map_fmap_proper `{Countable K} {A B : ofe} (f : A → B) n :
+Global Instance map_fmap_ne `{Countable K} {A B : ofe} (f : A → B) n :
   Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
 Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
-Global Instance map_zip_with_proper `{Countable K} {A B C : ofe} (f : A → B → C) n :
+Global Instance map_zip_with_ne `{Countable K} {A B C : ofe} (f : A → B → C) n :
   Proper (dist n ==> dist n ==> dist n) f →
   Proper (dist n ==> dist n ==> dist n) (map_zip_with (M:=gmap K) f).
 Proof.
-- 
GitLab