From 10d41e4e815482127748a45d5af08d0328f56025 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Tue, 26 Jul 2022 19:26:43 +0200
Subject: [PATCH] Fix the naming of kmap_subseteq and kmap_subset

---
 CHANGELOG.md        | 11 +++++++++++
 theories/fin_maps.v |  6 +++---
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2f4c0888..26ef6df1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,6 +21,17 @@ Coq 8.11 is no longer supported.
 - Declare `Hint Mode` for `FinSet A C` so that `C` is input, and `A` is output
   (i.e., inferred from `C`).
 - Add function `map_preimage` to compute the preimage of a finite map.
+- Rename `map_disjoint_subseteq` → `kmap_subseteq` and
+  `map_disjoint_subset` → `kmap_subset`.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bmap_disjoint_subseteq\b/kmap_subseteq/g
+s/\bmap_disjoint_subset\b/kmap_subset/g
+EOF
+```
 
 ## std++ 1.7.0 (2022-01-22)
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 720b154d..dc7cdc37 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -3265,14 +3265,14 @@ Section kmap.
   Proof.
     rewrite !map_disjoint_spec. setoid_rewrite lookup_kmap_Some. naive_solver.
   Qed.
-  Lemma map_disjoint_subseteq {A} (m1 m2 : M1 A) :
+  Lemma kmap_subseteq {A} (m1 m2 : M1 A) :
     kmap f m1 ⊆ kmap f m2 ↔ m1 ⊆ m2.
   Proof.
     rewrite !map_subseteq_spec. setoid_rewrite lookup_kmap_Some. naive_solver.
   Qed.
-  Lemma map_disjoint_subset {A} (m1 m2 : M1 A) :
+  Lemma kmap_subset {A} (m1 m2 : M1 A) :
     kmap f m1 ⊂ kmap f m2 ↔ m1 ⊂ m2.
-  Proof. unfold strict. by rewrite !map_disjoint_subseteq. Qed.
+  Proof. unfold strict. by rewrite !kmap_subseteq. Qed.
 End kmap.
 
 Section preimage.
-- 
GitLab