From 28af1927bc35519e95b2f2fc23a9a56c8e439a79 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 May 2022 10:15:44 +0200
Subject: [PATCH] =?UTF-8?q?DK=20=E2=86=92=20SK.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/fin_maps.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index eb264a2c..720b154d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -169,13 +169,13 @@ Global Instance map_lookup_total `{!Lookup K A (M A), !Inhabited A} :
 Typeclasses Opaque map_lookup_total.
 
 (** Given a finite map [m] with keys [K] and values [A], the preimage
-[map_preimage m] gives a finite map with keys [A] and values set [A]. The type
-of [map_preimage] is very generic to support different map and set
-implementations. A possible instance is [MKA:=gmap K A], [MADK:=gmap A (gset K)],
-and [DK:=gset K]. *)
-Definition map_preimage `{FinMapToList K A MKA, Empty MADK,
-    PartialAlter A DK MADK, Empty DK, Singleton K DK, Union DK}
-    (m : MKA) : MADK :=
+[map_preimage m] gives a finite map with keys [A] and values being sets of [K].
+The type of [map_preimage] is very generic to support different map and set
+implementations. A possible instance is [MKA:=gmap K A], [MASK:=gmap A (gset K)],
+and [SK:=gset K]. *)
+Definition map_preimage `{FinMapToList K A MKA, Empty MASK,
+    PartialAlter A SK MASK, Empty SK, Singleton K SK, Union SK}
+    (m : MKA) : MASK :=
   map_fold (λ i, partial_alter (λ mX, Some $ {[ i ]} ∪ default ∅ mX)) ∅ m.
 Typeclasses Opaque map_preimage.
 
@@ -3280,9 +3280,9 @@ Section preimage.
   sufficient for [gset], but not for [boolset] or [propset]. The result of the
   pre-image is a map of sets. To support general sets, we would need setoid
   equality on sets, and thus setoid equality on maps. *)
-  Context `{FinMap K MK, FinMap A MA, FinSet K DK, !LeibnizEquiv DK}.
+  Context `{FinMap K MK, FinMap A MA, FinSet K SK, !LeibnizEquiv SK}.
   Local Notation map_preimage :=
-    (map_preimage (K:=K) (A:=A) (MKA:=MK A) (MADK:=MA DK) (DK:=DK)).
+    (map_preimage (K:=K) (A:=A) (MKA:=MK A) (MASK:=MA SK) (SK:=SK)).
   Implicit Types m : MK A.
 
   Lemma map_preimage_empty : map_preimage ∅ = ∅.
-- 
GitLab