Skip to content

Type class inference issue with `dom` and `exist_fresh`

From stdpp Require Import fin_sets gmap.

Lemma foo (m : gmap nat nat) : True.
Proof.
  destruct (exist_fresh (dom m)).
(*
Unable to satisfy the following constraints:
In environment:
m : gmap nat nat

?Dom : "Dom (gmap nat nat) (mapset.mapset' (pmap.Pmap ()))"
*)

See examples@6480bf00 (comment 80689)

Edited by Robbert Krebbers