Merge branch 'robbert/issue_139' into 'master'

Set `Hint Mode` for `FinSet`.

Closes #139

See merge request iris/stdpp!379

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)
 

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.

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.