diff --git a/CHANGELOG.md b/CHANGELOG.md
index fe150cdc9b4adfff28678aaff2cbd9dfc7ec35a3..81e65e0efbaac527adc9df29866523b2fd03f23b 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 f2be1b2ae4f3b6ac7fb9c7d919471e94dc5f1061..4da774f931ce3e36173ada01da174020e0bf5f06 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.