From 59444525ae568543e3c1015cc77f913accf18db0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 Apr 2020 18:30:09 +0200
Subject: [PATCH] Rename `fin_maps.singleton_proper` into `singletonM_proper`.

---
 CHANGELOG.md        | 2 ++
 theories/fin_maps.v | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3346a6e3..b1d7e70a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -57,6 +57,8 @@ Noteworthy additions and changes:
     `seqZ_lookup_ge` → `lookup_seqZ_ge`, and `seqZ_lookup` → `lookup_seqZ`
   + Rename `lookup_seq_inv` → `lookup_seq` and generalize it to a bi-implication
   + Add `NoDup_seqZ` and `Forall_seqZ`
+- Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
+  `singletonM` and to avoid overlap with `sets.singleton_proper`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index eaab32fe..966c44e9 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -184,7 +184,7 @@ Section setoid.
   Global Instance insert_proper (i : K) :
     Proper ((≡) ==> (≡) ==> (≡@{M A})) (insert i).
   Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
-  Global Instance singleton_proper k : Proper ((≡) ==> (≡@{M A})) (singletonM k).
+  Global Instance singletonM_proper k : Proper ((≡) ==> (≡@{M A})) (singletonM k).
   Proof.
     intros ???; apply insert_proper; [done|].
     intros ?. rewrite lookup_empty; constructor.
-- 
GitLab