diff --git a/CHANGELOG.md b/CHANGELOG.md
index 712c4b8a2ab92ff96387d676d4c5c6c72cc8291a..c84a157f13bd6ce5a1d12ed5002c080fef0dc241 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,6 +18,8 @@ Coq 8.11 is no longer supported.
 - Rename "unsealing" lemmas from `_eq` to `_unseal`. This affects `ndot_eq` and
   `nclose_eq`. These unsealing lemmas are internal, so in principle you should
   not rely on them.
+- Declare `Hint Mode` for `FinSet A C` so that `C` is input, and `A` is output
+  (i.e., inferred from `C`).
 
 ## std++ 1.7.0 (2022-01-22)
 
diff --git a/tests/gmap.v b/tests/gmap.v
index 3eb98b0619ee09a6c29f59acc8ce10f4e8afb1b2..fff2df33a33d84a01b1ac8737b2974b467a1365d 100644
--- a/tests/gmap.v
+++ b/tests/gmap.v
@@ -82,3 +82,10 @@ Proof.
   Fail progress simplify_eq.
   done.
 Qed.
+
+(** Test case for issue #139 *)
+
+Lemma test_issue_139 (m : gmap nat nat) : ∃ x, x ∉ dom m.
+Proof.
+  destruct (exist_fresh (dom m)); eauto.
+Qed.
diff --git a/theories/base.v b/theories/base.v
index a09cd676ff7b92e32dd709ab3e11fa3df9047aba..f8105fb370340d9d345f7bb22484d130e70b4742 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1468,6 +1468,8 @@ Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
   elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
   NoDup_elements (X : C) : NoDup (elements X)
 }.
+Global Hint Mode FinSet - ! - - - - - - - - : typeclass_instances.
+
 Class Size C := size: C → nat.
 Global Hint Mode Size ! : typeclass_instances.
 Global Arguments size {_ _} !_ / : simpl nomatch, assert.