changelog and FIXME

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)
 

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.