From 71bce7f8ea6c3822fc29263bb2338948fe01c8d7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Jul 2021 12:48:16 +0200
Subject: [PATCH] =?UTF-8?q?rename=20map=5Funion=5Fsubseteq=5Fl=5Falt=20?=
 =?UTF-8?q?=E2=86=92=20map=5Funion=5Fsubseteq=5Fl'=20(and=20likewise=20for?=
 =?UTF-8?q?=20=5Fr)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md        | 5 +++++
 theories/fin_maps.v | 4 ++--
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2d590c01..80dd8afd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -116,6 +116,9 @@ API-breaking change is listed.
 - Swap names of `curry`/`uncurry`, `curry3`/`uncurry3`, `curry4`/`uncurry4`,
   `gmap_curry`/`gmap_uncurry`, and `hcurry`/`huncurry` to be consistent with
   Haskell and friends.
+- Rename `map_union_subseteq_l_alt` → `map_union_subseteq_l'` and
+  `map_union_subseteq_r_alt` → `map_union_subseteq_r'` to be consistent with
+  `or_intro_{l,r}'`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -156,6 +159,8 @@ s/\bgmap_uncurry_non_empty\b/gmap_curry_non_empty/g
 s/\bgmap_uncurry_curry_non_empty\b/gmap_curry_uncurry_non_empty/g
 s/\bhcurry_uncurry\b/huncurry_curry/g
 s/\blookup_gmap_uncurry_None\b/lookup_gmap_curry_None/g
+# map_union_subseteq
+s/\bmap_union_subseteq_(r|l)_alt\b/map_union_subseteq_\1'/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 920b9426..9c8ff8b9 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2039,9 +2039,9 @@ Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 ##ₘ m2 → m2 ⊆ m1 ∪ m2.
 Proof.
   intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
 Qed.
-Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
+Lemma map_union_subseteq_l' {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
 Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
-Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
+Lemma map_union_subseteq_r' {A} (m1 m2 m3 : M A) :
   m2 ##ₘ m3 → m1 ⊆ m3 → m1 ⊆ m2 ∪ m3.
 Proof. intros. trans m3; auto using map_union_subseteq_r. Qed.
 Lemma map_union_mono_l {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m3 ∪ m1 ⊆ m3 ∪ m2.
-- 
GitLab