stdpp/base.v

@@ -364,7 +364,7 @@ an explicit class instead of a notation for two reasons:
   unnecessary evaluation. *)
 Class RelDecision {A B} (R : A → B → Prop) :=
   decide_rel x y :> Decision (R x y).
-Global Hint Mode RelDecision ! ! ! : typeclass_instances.
+Global Hint Mode RelDecision + + ! : typeclass_instances.
 Global Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
 Notation EqDecision A := (RelDecision (=@{A})).
 
@@ -968,13 +968,13 @@ relations on sets: the empty set [∅], the union [(∪)],
 intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 [(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
 Class Empty A := empty: A.
-Global Hint Mode Empty ! : typeclass_instances.
+Global Hint Mode Empty + : typeclass_instances.
 Notation "∅" := empty (format "∅") : stdpp_scope.
 
 Global Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
 
 Class Union A := union: A → A → A.
-Global Hint Mode Union ! : typeclass_instances.
+Global Hint Mode Union + : typeclass_instances.
 Global Instance: Params (@union) 2 := {}.
 Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
 Notation "(∪)" := union (only parsing) : stdpp_scope.
@@ -988,7 +988,7 @@ Global Arguments union_list _ _ _ !_ / : assert.
 Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
 
 Class Intersection A := intersection: A → A → A.
-Global Hint Mode Intersection ! : typeclass_instances.
+Global Hint Mode Intersection + : typeclass_instances.
 Global Instance: Params (@intersection) 2 := {}.
 Infix "∩" := intersection (at level 40) : stdpp_scope.
 Notation "(∩)" := intersection (only parsing) : stdpp_scope.
@@ -996,7 +996,7 @@ Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope.
 Notation "(.∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
 
 Class Difference A := difference: A → A → A.
-Global Hint Mode Difference ! : typeclass_instances.
+Global Hint Mode Difference + : typeclass_instances.
 Global Instance: Params (@difference) 2 := {}.
 Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
 Notation "(∖)" := difference (only parsing) : stdpp_scope.
@@ -1014,7 +1014,7 @@ Notation "{[ x ; y ; .. ; z ]}" :=
   (at level 1) : stdpp_scope.
 
 Class SubsetEq A := subseteq: relation A.
-Global Hint Mode SubsetEq ! : typeclass_instances.
+Global Hint Mode SubsetEq + : typeclass_instances.
 Global Instance: Params (@subseteq) 2 := {}.
 Infix "⊆" := subseteq (at level 70) : stdpp_scope.
 Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
@@ -1061,7 +1061,7 @@ and define [{[+ x1; ..; xn +]}] as [{[ x1 ]} ⊎ .. ⊎ {[ xn ]}]. However, this
 would risk accidentally using [{[ x1; ..; xn ]}] for multisets (leading to
 unexpected results) and lead to ambigious pretty printing for [{[+ x +]}]. *)
 Class DisjUnion A := disj_union: A → A → A.
-Global Hint Mode DisjUnion ! : typeclass_instances.
+Global Hint Mode DisjUnion + : typeclass_instances.
 Global Instance: Params (@disj_union) 2 := {}.
 Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
 Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
@@ -1069,7 +1069,8 @@ Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
 Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
 
 Class SingletonMS A B := singletonMS: A → B.
-Global Hint Mode SingletonMS - ! : typeclass_instances.
+Global Hint Mode SingletonMS + ! : typeclass_instances.
+Global Hint Mode SingletonMS - + : typeclass_instances.
 Global Instance: Params (@singletonMS) 3 := {}.
 Notation "{[+ x +]}" := (singletonMS x)
   (at level 1, format "{[+  x  +]}") : stdpp_scope.
@@ -1088,10 +1089,11 @@ Fixpoint list_to_set_disj `{SingletonMS A C, Empty C, DisjUnion C} (l : list A)
 is used to create finite maps, finite sets, etc, and is typically different from
 the order [(⊆)]. *)
 Class Lexico A := lexico: relation A.
-Global Hint Mode Lexico ! : typeclass_instances.
+Global Hint Mode Lexico + : typeclass_instances.
 
 Class ElemOf A B := elem_of: A → B → Prop.
-Global Hint Mode ElemOf - ! : typeclass_instances.
+Global Hint Mode ElemOf + ! : typeclass_instances.
+Global Hint Mode ElemOf - + : typeclass_instances.
 Global Instance: Params (@elem_of) 3 := {}.
 Infix "∈" := elem_of (at level 70) : stdpp_scope.
 Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
@@ -1109,7 +1111,7 @@ Notation "x ∉@{ B } X" := (¬x ∈@{B} X) (at level 80, only parsing) : stdpp_
 Notation "(∉@{ B } )" := (λ x X, x ∉@{B} X) (only parsing) : stdpp_scope.
 
 Class Disjoint A := disjoint : A → A → Prop.
-Global Hint Mode Disjoint ! : typeclass_instances.
+Global Hint Mode Disjoint + : typeclass_instances.
 Global Instance: Params (@disjoint) 2 := {}.
 Infix "##" := disjoint (at level 70) : stdpp_scope.
 Notation "(##)" := disjoint (only parsing) : stdpp_scope.
@@ -1126,10 +1128,12 @@ Global Hint Extern 0 (_ ## _) => symmetry; eassumption : core.
 Global Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
 
 Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
-Global Hint Mode Filter - ! : typeclass_instances.
+Global Hint Mode Filter + ! : typeclass_instances.
+Global Hint Mode Filter - + : typeclass_instances.
 
 Class UpClose A B := up_close : A → B.
-Global Hint Mode UpClose - ! : typeclass_instances.
+Global Hint Mode UpClose + ! : typeclass_instances.
+Global Hint Mode UpClose - + : typeclass_instances.
 Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 
 (** * Monadic operations *)
@@ -1140,27 +1144,27 @@ class with the monad laws). *)
 Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
 Global Arguments mret {_ _ _} _ : assert.
 Global Instance: Params (@mret) 3 := {}.
-Global Hint Mode MRet ! : typeclass_instances.
+Global Hint Mode MRet + : typeclass_instances.
 
 Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
 Global Arguments mbind {_ _ _ _} _ !_ / : assert.
 Global Instance: Params (@mbind) 4 := {}.
-Global Hint Mode MBind ! : typeclass_instances.
+Global Hint Mode MBind + : typeclass_instances.
 
 Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
 Global Arguments mjoin {_ _ _} !_ / : assert.
 Global Instance: Params (@mjoin) 3 := {}.
-Global Hint Mode MJoin ! : typeclass_instances.
+Global Hint Mode MJoin + : typeclass_instances.
 
 Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
 Global Arguments fmap {_ _ _ _} _ !_ / : assert.
 Global Instance: Params (@fmap) 4 := {}.
-Global Hint Mode FMap ! : typeclass_instances.
+Global Hint Mode FMap + : typeclass_instances.
 
 Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
 Global Arguments omap {_ _ _ _} _ !_ / : assert.
 Global Instance: Params (@omap) 4 := {}.
-Global Hint Mode OMap ! : typeclass_instances.
+Global Hint Mode OMap + : typeclass_instances.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
 Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
@@ -1197,7 +1201,8 @@ Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
 on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function look up [m !! k] should yield the element at key [k] in [m]. *)
 Class Lookup (K A M : Type) := lookup: K → M → option A.
-Global Hint Mode Lookup - - ! : typeclass_instances.
+Global Hint Mode Lookup - + ! : typeclass_instances.
+Global Hint Mode Lookup - - + : typeclass_instances.
 Global Instance: Params (@lookup) 4 := {}.
 Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
 Notation "(!!)" := lookup (only parsing) : stdpp_scope.
@@ -1208,7 +1213,8 @@ Global Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 (** The function [lookup_total] should be the total over-approximation
 of the partial [lookup] function. *)
 Class LookupTotal (K A M : Type) := lookup_total : K → M → A.
-Global Hint Mode LookupTotal - - ! : typeclass_instances.
+Global Hint Mode LookupTotal - + ! : typeclass_instances.
+Global Hint Mode LookupTotal - - + : typeclass_instances.
 Global Instance: Params (@lookup_total) 4 := {}.
 Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope.
 Notation "(!!!)" := lookup_total (only parsing) : stdpp_scope.
@@ -1218,14 +1224,16 @@ Global Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The singleton map *)
 Class SingletonM K A M := singletonM: K → A → M.
-Global Hint Mode SingletonM - - ! : typeclass_instances.
+Global Hint Mode SingletonM - + ! : typeclass_instances.
+Global Hint Mode SingletonM - - + : typeclass_instances.
 Global Instance: Params (@singletonM) 5 := {}.
 Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
 Class Insert (K A M : Type) := insert: K → A → M → M.
-Global Hint Mode Insert - - ! : typeclass_instances.
+Global Hint Mode Insert - + ! : typeclass_instances.
+Global Hint Mode Insert - - + : typeclass_instances.
 Global Instance: Params (@insert) 5 := {}.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
@@ -1304,14 +1312,15 @@ Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)
 Class Delete (K M : Type) := delete: K → M → M.
-Global Hint Mode Delete - ! : typeclass_instances.
+Global Hint Mode Delete - + : typeclass_instances.
 Global Instance: Params (@delete) 4 := {}.
 Global Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
-Global Hint Mode Alter - - ! : typeclass_instances.
+Global Hint Mode Alter - + ! : typeclass_instances.
+Global Hint Mode Alter - - + : typeclass_instances.
 Global Instance: Params (@alter) 4 := {}.
 Global Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
@@ -1321,7 +1330,8 @@ if [k] is not a member of [m]. The value at [k] should be deleted if [f]
 yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
-Global Hint Mode PartialAlter - - ! : typeclass_instances.
+Global Hint Mode PartialAlter - + ! : typeclass_instances.
+Global Hint Mode PartialAlter - - + : typeclass_instances.
 Global Instance: Params (@partial_alter) 4 := {}.
 Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
@@ -1330,7 +1340,7 @@ set of type [D] that contains the keys that are a member of [m].
 [D] is an output of the typeclass, i.e., there can be only one instance per map
 type [M]. *)
 Class Dom (M D : Type) := dom: M → D.
-Global Hint Mode Dom ! - : typeclass_instances.
+Global Hint Mode Dom + - : typeclass_instances.
 Global Instance: Params (@dom) 3 := {}.
 Global Arguments dom : clear implicits.
 Global Arguments dom {_ _ _} !_ / : simpl nomatch, assert.
@@ -1339,7 +1349,7 @@ Global Arguments dom {_ _ _} !_ / : simpl nomatch, assert.
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
 Class Merge (M : Type → Type) :=
   merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
-Global Hint Mode Merge ! : typeclass_instances.
+Global Hint Mode Merge + : typeclass_instances.
 Global Instance: Params (@merge) 4 := {}.
 Global Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
@@ -1348,20 +1358,23 @@ and [m2] using the function [f] to combine values of members that are in
 both [m1] and [m2]. *)
 Class UnionWith (A M : Type) :=
   union_with: (A → A → option A) → M → M → M.
-Global Hint Mode UnionWith - ! : typeclass_instances.
+Global Hint Mode UnionWith + ! : typeclass_instances.
+Global Hint Mode UnionWith - + : typeclass_instances.
 Global Instance: Params (@union_with) 3 := {}.
 Global Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** Similarly for intersection and difference. *)
 Class IntersectionWith (A M : Type) :=
   intersection_with: (A → A → option A) → M → M → M.
-Global Hint Mode IntersectionWith - ! : typeclass_instances.
+Global Hint Mode IntersectionWith + ! : typeclass_instances.
+Global Hint Mode IntersectionWith - + : typeclass_instances.
 Global Instance: Params (@intersection_with) 3 := {}.
 Global Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Class DifferenceWith (A M : Type) :=
   difference_with: (A → A → option A) → M → M → M.
-Global Hint Mode DifferenceWith - ! : typeclass_instances.
+Global Hint Mode DifferenceWith + ! : typeclass_instances.
+Global Hint Mode DifferenceWith - + : typeclass_instances.
 Global Instance: Params (@difference_with) 3 := {}.
 Global Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
@@ -1373,7 +1386,7 @@ Global Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
 (** SqSubsetEq registers the "canonical" partial order for a type, and is used
 for the \sqsubseteq symbol. *)
 Class SqSubsetEq A := sqsubseteq: relation A.
-Global Hint Mode SqSubsetEq ! : typeclass_instances.
+Global Hint Mode SqSubsetEq + : typeclass_instances.
 Global Instance: Params (@sqsubseteq) 2 := {}.
 Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
 Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
@@ -1391,7 +1404,7 @@ Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) |
 Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.
 
 Class Meet A := meet: A → A → A.
-Global Hint Mode Meet ! : typeclass_instances.
+Global Hint Mode Meet + : typeclass_instances.
 Global Instance: Params (@meet) 2 := {}.
 Infix "⊓" := meet (at level 40) : stdpp_scope.
 Notation "(⊓)" := meet (only parsing) : stdpp_scope.
@@ -1399,7 +1412,7 @@ Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
 Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
 
 Class Join A := join: A → A → A.
-Global Hint Mode Join ! : typeclass_instances.
+Global Hint Mode Join + : typeclass_instances.
 Global Instance: Params (@join) 2 := {}.
 Infix "⊔" := join (at level 50) : stdpp_scope.
 Notation "(⊔)" := join (only parsing) : stdpp_scope.
@@ -1407,11 +1420,11 @@ Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
 Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
 
 Class Top A := top : A.
-Global Hint Mode Top ! : typeclass_instances.
+Global Hint Mode Top + : typeclass_instances.
 Notation "⊤" := top (format "⊤") : stdpp_scope.
 
 Class Bottom A := bottom : A.
-Global Hint Mode Bottom ! : typeclass_instances.
+Global Hint Mode Bottom + : typeclass_instances.
 Notation "⊥" := bottom (format "⊥") : stdpp_scope.
 
 
@@ -1431,7 +1444,7 @@ Class SemiSet A C `{ElemOf A C,
   elem_of_singleton (x y : A) : x ∈@{C} {[ y ]} ↔ x = y;
   elem_of_union (X Y : C) (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
 }.
-Global Hint Mode SemiSet - ! - - - - : typeclass_instances.
+Global Hint Mode SemiSet - + - - - - : typeclass_instances.
 
 Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
@@ -1439,7 +1452,7 @@ Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
   elem_of_intersection (X Y : C) (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
   elem_of_difference (X Y : C) (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
-Global Hint Mode Set_ - ! - - - - - - : typeclass_instances.
+Global Hint Mode Set_ - + - - - - - - : typeclass_instances.
 
 Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
@@ -1447,13 +1460,14 @@ Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
   elem_of_top' (x : A) : x ∈@{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
   in [sets.v], which is more convenient for rewriting. *)
 }.
-Global Hint Mode TopSet - ! - - - - - - - : typeclass_instances.
+Global Hint Mode TopSet - + - - - - - - - : typeclass_instances.
 
 (** We axiomative a finite set as a set whose elements can be
 enumerated as a list. These elements, given by the [elements] function, may be
 in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
-Global Hint Mode Elements - ! : typeclass_instances.
+Global Hint Mode Elements + ! : typeclass_instances.
+Global Hint Mode Elements - + : typeclass_instances.
 Global Instance: Params (@elements) 3 := {}.
 
 (** We redefine the standard library's [In] and [NoDup] using type classes. *)
@@ -1488,10 +1502,10 @@ 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.
+Global Hint Mode FinSet - + - - - - - - - - : typeclass_instances.
 
 Class Size C := size: C → nat.
-Global Hint Mode Size ! : typeclass_instances.
+Global Hint Mode Size + : typeclass_instances.
 Global Arguments size {_ _} !_ / : simpl nomatch, assert.
 Global Instance: Params (@size) 2 := {}.
 
@@ -1534,7 +1548,8 @@ aforementioned [fresh] function on finite sets that respects set equality.
 Instead of instantiating [Infinite] directly, consider using [max_infinite] or
 [inj_infinite] from the [infinite] module. *)
 Class Fresh A C := fresh: C → A.
-Global Hint Mode Fresh - ! : typeclass_instances.
+Global Hint Mode Fresh + ! : typeclass_instances.
+Global Hint Mode Fresh - + : typeclass_instances.
 Global Instance: Params (@fresh) 3 := {}.
 Global Arguments fresh : simpl never.
 
@@ -1543,11 +1558,11 @@ Class Infinite A := {
   infinite_is_fresh (xs : list A) : fresh xs ∉ xs;
   infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh;
 }.
-Global Hint Mode Infinite ! : typeclass_instances.
+Global Hint Mode Infinite + : typeclass_instances.
 Global Arguments infinite_fresh : simpl never.
 
 (** * Miscellaneous *)
 Class Half A := half: A → A.
-Global Hint Mode Half ! : typeclass_instances.
+Global Hint Mode Half + : typeclass_instances.
 Notation "½" := half (format "½") : stdpp_scope.
 Notation "½*" := (fmap (M:=list) half) : stdpp_scope.

stdpp/coPset.v

@@ -215,7 +215,7 @@ Fixpoint coPset_finite (t : coPset_raw) : bool :=
 Lemma coPset_finite_node b l r :
   coPset_finite (coPNode' b l r) = coPset_finite l && coPset_finite r.
 Proof. by destruct b, l as [[]|], r as [[]|]. Qed.
-Lemma coPset_finite_spec X : set_finite X ↔ coPset_finite (`X).
+Lemma coPset_finite_spec (X : coPset) : set_finite X ↔ coPset_finite (`X).
 Proof.
   destruct X as [t Ht].
   unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.

stdpp/countable.v

@@ -14,7 +14,7 @@ Class Countable A `{EqDecision A} := {
   decode : positive → option A;
   decode_encode x : decode (encode x) = Some x
 }.
-Global Hint Mode Countable ! - : typeclass_instances.
+Global Hint Mode Countable + - : typeclass_instances.
 Global Arguments encode : simpl never.
 Global Arguments decode : simpl never.
 

stdpp/fin_maps.v

@@ -27,8 +27,8 @@ which enables us to give a generic implementation of [union_with],
 [intersection_with], and [difference_with]. *)
 
 Class FinMapToList K A M := map_to_list: M → list (K * A).
-Global Hint Mode FinMapToList ! - - : typeclass_instances.
-Global Hint Mode FinMapToList - - ! : typeclass_instances.
+Global Hint Mode FinMapToList + - - : typeclass_instances.
+Global Hint Mode FinMapToList - - + : typeclass_instances.
 
 (** The function [diag_None f] is used in the specification and lemmas of
 [merge f]. It lifts a function [f : option A → option B → option C] by returning

stdpp/gmap.v

@@ -43,7 +43,8 @@ Defined.
 (** * Operations on the data structure *)
 Global Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) :=
   λ i '(GMap m _), m !! encode i.
-Global Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
+Global Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) :=
+  GMap (∅ : Pmap A) I.
 (** Block reduction, even on concrete [gmap]s.
 Marking [gmap_empty] as [simpl never] would not be enough, because of
 https://github.com/coq/coq/issues/2972 and

stdpp/listset.v

@@ -24,7 +24,7 @@ Proof.
   - by apply elem_of_list_singleton.
   - intros [?] [?]. apply elem_of_app.
 Qed.
-Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
+Lemma listset_empty_alt (X : listset A) : X ≡ ∅ ↔ listset_car X = [].
 Proof.
   destruct X as [l]; split; [|by intros; simplify_eq/=].
   rewrite elem_of_equiv_empty; intros Hl.

stdpp/pmap.v

@@ -186,7 +186,7 @@ Proof.
       { left; exists (i' ~ 0). by rewrite Pos.reverse_xO, (assoc_L _). }
       destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
       left; exists (i' ~ 1). by rewrite Pos.reverse_xI, (assoc_L _). }
-  revert t j i acc. assert (∀ t j i acc,
+  revert t j i acc. assert (∀ (t : Pmap_raw A) j i acc,
     (i, x) ∈ acc → (i, x) ∈ Pto_list_raw j t acc) as help.
   { intros t; induction t as [|[y|] l IHl r IHr]; intros j i acc;
       simpl; rewrite ?elem_of_cons; auto. }
@@ -269,7 +269,7 @@ Global Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
   | left H => left (proj2 (Pmap_eq m1 m2) H)
   | right H => right (H ∘ proj1 (Pmap_eq m1 m2))
   end.
-Global Instance Pempty {A} : Empty (Pmap A) := PMap ∅ I.
+Global Instance Pempty {A} : Empty (Pmap A) := PMap Pempty_raw I.
 Global Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
 Global Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
   let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).