From 58458a53dbe9510d66615921a64deceff2663fae Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 30 May 2022 08:13:49 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)
---
theories/fin_maps.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index abf730e1..eb264a2c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -3278,8 +3278,8 @@ End kmap.
Section preimage.
(** We restrict the theory to finite sets with Leibniz equality, which is
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 need setoid equality
- on sets, and thus setoid equality on maps. *)
+ 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}.
Local Notation map_preimage :=
(map_preimage (K:=K) (A:=A) (MKA:=MK A) (MADK:=MA DK) (DK:=DK)).
--
GitLab