From 6b885cdd7242189480d538d12263c8ead635bf67 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 May 2022 08:25:09 +0200
Subject: [PATCH] changelog and FIXME

---
 CHANGELOG.md           | 7 +++++++
 theories/fin_map_dom.v | 1 +
 2 files changed, 8 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fe150cdc..81e65e0e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,13 @@ Coq 8.11 is no longer supported.
 
 - Make sure that `gset` and `mapset` do not bump the universe.
 - Rewrite `tele_arg` to make it not bump universes. (by Gregory Malecha, BedRock Systems)
+- Change `dom D M` (where `D` is the domain type) to `dom M`; the domain type is
+  now inferred automatically. To make this possible, getting the domain of a
+  `gmap` as a `coGset` and of a `Pmap` as a `coPset` is no longer supported. Use
+  `gset_to_coGset`/`Pset_to_coPset` instead.
+  When combining `dom` with `≡`, this can run into an old issue (due to a Coq
+  issue, `Equiv` does not the desired `Hint Mode !`), which can make it
+  necessary to annotate the set type at the `≡` via `≡@{D}`.
 
 ## std++ 1.7.0 (2022-01-22)
 
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index f2be1b2a..4da774f9 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -66,6 +66,7 @@ Lemma dom_filter_subseteq {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m
   dom (filter P m) ⊆ dom m.
 Proof. apply subseteq_dom, map_filter_subseteq. Qed.
 
+(* FIXME: Once [Equiv] has [Mode !], we can remove all these [D] type annotations at [≡]. *)
 Lemma dom_empty {A} : dom (@empty (M A) _) ≡@{D} ∅.
 Proof.
   intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
-- 
GitLab