diff --git a/theories/base.v b/theories/base.v
index 40e58b18e03938ce2d4609b283940333f6b41dfe..b046cf8e814a59f69444b04f98611140c266b996 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -785,7 +785,7 @@ Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
 (** In this section we define operational type classes for the operations
 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 : Type) (M : Type → Type) := lookup : ∀ {A}, K → M A → option A.
+Class Lookup (K A M : Type) := lookup: K → M → option A.
 Instance: Params (@lookup) 4.
 Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
 Notation "(!!)" := lookup (only parsing) : C_scope.
@@ -794,14 +794,13 @@ Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
 Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** The singleton map *)
-Class SingletonM (K : Type) (M : Type → Type) :=
-  singletonM : ∀ {A}, K → A → M A.
+Class SingletonM K A M := singletonM: K → A → M.
 Instance: Params (@singletonM) 5.
 Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : C_scope.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
-Class Insert (K : Type) (M : Type → Type) := insert : ∀ {A}, K → A → M A → M A.
+Class Insert (K A M : Type) := insert: K → A → M → M.
 Instance: Params (@insert) 5.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
@@ -810,14 +809,13 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
 (** The function delete [delete k m] should delete the value at key [k] in
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)
-Class Delete (K : Type) (M : Type → Type) := delete : ∀ {A}, K → M A → M A.
-Instance: Params (@delete) 5.
-Arguments delete _ _ _ _ !_ !_ / : simpl nomatch.
+Class Delete (K M : Type) := delete: K → M → M.
+Instance: Params (@delete) 4.
+Arguments delete _ _ _ !_ !_ / : simpl nomatch.
 
 (** 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 : Type) (M : Type → Type) :=
-  alter : ∀ {A}, (A → A) → K → M A → M A.
+Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
 Instance: Params (@alter) 5.
 Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
 
@@ -825,16 +823,16 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
 function [f], which is called with the original value at key [k] or [None]
 if [k] is not a member of [m]. The value at [k] should be deleted if [f] 
 yields [None]. *)
-Class PartialAlter (K : Type) (M : Type → Type) :=
-  partial_alter : ∀ {A}, (option A → option A) → K → M A → M A.
+Class PartialAlter (K A M : Type) :=
+  partial_alter: (option A → option A) → K → M → M.
 Instance: Params (@partial_alter) 4.
 Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function [dom C m] should yield the domain of [m]. That is a finite
 collection of type [C] that contains the keys that are a member of [m]. *)
-Class Dom (M : Type → Type) (C : Type) := dom : ∀ {A}, M A → C.
-Instance: Params (@dom) 4.
-Arguments dom {_} _ {_ _} !_ / : simpl nomatch, clear implicits.
+Class Dom (M C : Type) := dom: M → C.
+Instance: Params (@dom) 3.
+Arguments dom {_} _ {_} !_ / : simpl nomatch, clear implicits.
 
 (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
@@ -846,27 +844,39 @@ Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch.
 (** The function [union_with f m1 m2] is supposed to yield the union of [m1]
 and [m2] using the function [f] to combine values of members that are in
 both [m1] and [m2]. *)
-Class UnionWith (M : Type → Type) :=
-  union_with : ∀ {A}, (A → A → option A) → M A → M A → M A.
+Class UnionWith (A M : Type) :=
+  union_with: (A → A → option A) → M → M → M.
 Instance: Params (@union_with) 3.
 Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch.
 
 (** Similarly for intersection and difference. *)
-Class IntersectionWith (M : Type → Type) :=
-  intersection_with : ∀ {A}, (A → A → option A) → M A → M A → M A.
+Class IntersectionWith (A M : Type) :=
+  intersection_with: (A → A → option A) → M → M → M.
 Instance: Params (@intersection_with) 3.
 Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch.
 
-Class DifferenceWith (M : Type → Type) :=
-  difference_with : ∀ {A}, (A → A → option A) → M A → M A → M A.
+Class DifferenceWith (A M : Type) :=
+  difference_with: (A → A → option A) → M → M → M.
 Instance: Params (@difference_with) 3.
 Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch.
 
-Definition intersection_with_list `{IntersectionWith M} {A}
-    (f : A → A → option A) : M A → list (M A) → M A :=
-  fold_right (intersection_with f).
+Definition intersection_with_list `{IntersectionWith A M}
+  (f : A → A → option A) : M → list M → M := fold_right (intersection_with f).
 Arguments intersection_with_list _ _ _ _ _ !_ /.
 
+Class LookupE (E K A M : Type) := lookupE: E → K → M → option A.
+Instance: Params (@lookupE) 6.
+Notation "m !!{ Γ } i" := (lookupE Γ i m)
+  (at level 20, format "m  !!{ Γ }  i") : C_scope.
+Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : C_scope.
+Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch.
+
+Class InsertE (E K A M : Type) := insertE: E → K → A → M → M.
+Instance: Params (@insertE) 6.
+Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
+  (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
+Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.
+
 
 (** * Axiomatization of collections *)
 (** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
diff --git a/theories/coPset.v b/theories/coPset.v
index 2c5d25a26ca86f099b17cef2c211dff627e60f9e..b1086528f545827ae046ea7731f766a8d7ba1c90 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -326,13 +326,13 @@ Proof.
 Qed.
 
 (** * Domain of finite maps *)
-Instance Pmap_dom_coPset : Dom Pmap coPset := λ A m, of_Pset (dom _ m).
+Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, of_Pset (dom _ m).
 Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
 Proof.
   split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
   by rewrite elem_of_of_Pset, elem_of_dom.
 Qed.
-Instance gmap_dom_coPset : Dom (gmap positive) coPset := λ A m,
+Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
   of_gset (dom _ m).
 Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
 Proof.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index e17c7251fb85a512fb4af93f540c7b0c62ffb1b9..c3bfa075b398e2501de771a2171034ca9ba62117 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -5,9 +5,10 @@ maps. We provide such an axiomatization, instead of implementing the domain
 function in a generic way, to allow more efficient implementations. *)
 From stdpp Require Export collections fin_maps.
 
-Class FinMapDom K M D `{FMap M, Lookup K M, ∀ A, Empty (M A), PartialAlter K M,
-    OMap M, Merge M, FinMapToList K M, ∀ i j : K, Decision (i = j),
-    Dom M D, ElemOf K D, Empty D, Singleton K D,
+Class FinMapDom K M D `{FMap M,
+    ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
+    OMap M, Merge M, ∀ A, FinMapToList K A (M A), ∀ i j : K, Decision (i = j),
+    ∀ A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D,
     Union D, Intersection D, Difference D} := {
   finmap_dom_map :>> FinMap K M;
   finmap_dom_collection :>> Collection K D;
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a0ffd1d5fb98e2334c8995edb6d972586de9a5d2..da4e7f9940082143ae5560ef1380a5354fe6d927 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -23,11 +23,11 @@ prove well founded recursion on finite maps. *)
 which enables us to give a generic implementation of [union_with],
 [intersection_with], and [difference_with]. *)
 
-Class FinMapToList (K : Type) (M : Type → Type) :=
-  map_to_list : ∀ {A}, M A → list (K * A).
+Class FinMapToList K A M := map_to_list: M → list (K * A).
 
-Class FinMap K M `{FMap M, Lookup K M, ∀ A, Empty (M A), PartialAlter K M,
-    OMap M, Merge M, FinMapToList K M, ∀ i j : K, Decision (i = j)} := {
+Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
+    PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A),
+    ∀ i j : K, Decision (i = j)} := {
   map_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2;
   lookup_empty {A} i : (∅ : M A) !! i = None;
   lookup_partial_alter {A} f (m : M A) i :
@@ -48,47 +48,47 @@ Class FinMap K M `{FMap M, Lookup K M, ∀ A, Empty (M A), PartialAlter K M,
 finite map implementations. These generic implementations do not cause a
 significant performance loss to make including them in the finite map interface
 worthwhile. *)
-Instance map_insert `{PartialAlter K M} : Insert K M :=
-  λ A i x, partial_alter (λ _, Some x) i.
-Instance map_alter `{PartialAlter K M} : Alter K M :=
-  λ A f, partial_alter (fmap f).
-Instance map_delete `{PartialAlter K M} : Delete K M :=
-  λ A, partial_alter (λ _, None).
-Instance map_singleton `{PartialAlter K M, ∀ A, Empty (M A)} : SingletonM K M :=
-  λ A i x, <[i:=x]> ∅.
+Instance map_insert `{PartialAlter K A M} : Insert K A M :=
+  λ i x, partial_alter (λ _, Some x) i.
+Instance map_alter `{PartialAlter K A M} : Alter K A M :=
+  λ f, partial_alter (fmap f).
+Instance map_delete `{PartialAlter K A M} : Delete K M :=
+  partial_alter (λ _, None).
+Instance map_singleton `{PartialAlter K A M, Empty M} :
+  SingletonM K A M := λ i x, <[i:=x]> ∅.
 
-Definition map_of_list `{Insert K M, Empty (M A)} : list (K * A) → M A :=
+Definition map_of_list `{Insert K A M, Empty M} : list (K * A) → M :=
   fold_right (λ p, <[p.1:=p.2]>) ∅.
-Definition map_of_collection `{Elements K C, Insert K M, Empty (M A)}
-    (f : K → option A) (X : C) : M A :=
+Definition map_of_collection `{Elements K C, Insert K A M, Empty M}
+    (f : K → option A) (X : C) : M :=
   map_of_list (omap (λ i, (i,) <$> f i) (elements X)).
 
-Instance map_union_with `{Merge M} : UnionWith M :=
-  λ A f, merge (union_with f).
-Instance map_intersection_with `{Merge M} : IntersectionWith M :=
-  λ A f, merge (intersection_with f).
-Instance map_difference_with `{Merge M} : DifferenceWith M :=
-  λ A f, merge (difference_with f).
+Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
+  λ f, merge (union_with f).
+Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
+  λ f, merge (intersection_with f).
+Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
+  λ f, merge (difference_with f).
 
-Instance map_equiv `{Lookup K M, Equiv A} : Equiv (M A) | 18 :=
+Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 18 :=
   λ m1 m2, ∀ i, m1 !! i ≡ m2 !! i.
 
 (** The relation [intersection_forall R] on finite maps describes that the
 relation [R] holds for each pair in the intersection. *)
-Definition map_Forall `{Lookup K M} {A} (P : K → A → Prop) : M A → Prop :=
+Definition map_Forall `{Lookup K A M} (P : K → A → Prop) : M → Prop :=
   λ m, ∀ i x, m !! i = Some x → P i x.
-Definition map_relation `{Lookup K M} {A B} (R : A → B → Prop)
+Definition map_relation `{∀ A, Lookup K A (M A)} {A B} (R : A → B → Prop)
     (P : A → Prop) (Q : B → Prop) (m1 : M A) (m2 : M B) : Prop := ∀ i,
   option_relation R P Q (m1 !! i) (m2 !! i).
-Definition map_included `{Lookup K M} {A}
+Definition map_included `{∀ A, Lookup K A (M A)} {A}
   (R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
-Definition map_disjoint `{Lookup K M} {A} : relation (M A) :=
+Definition map_disjoint `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
   map_relation (λ _ _, False) (λ _, True) (λ _, True).
 Infix "⊥ₘ" := map_disjoint (at level 70) : C_scope.
 Hint Extern 0 (_ ⊥ₘ _) => symmetry; eassumption.
 Notation "( m ⊥ₘ.)" := (map_disjoint m) (only parsing) : C_scope.
 Notation "(.⊥ₘ m )" := (λ m2, m2 ⊥ₘ m) (only parsing) : C_scope.
-Instance map_subseteq `{Lookup K M} {A} : SubsetEq (M A) :=
+Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
   map_included (=).
 
 (** The union of two finite maps only has a meaningful definition for maps
@@ -106,8 +106,8 @@ Instance map_difference `{Merge M} {A} : Difference (M A) :=
 
 (** A stronger variant of map that allows the mapped function to use the index
 of the elements. Implemented by conversion to lists, so not very efficient. *)
-Definition map_imap `{Insert K M, ∀ A, Empty (M A),
-    FinMapToList K M} {A B} (f : K → A → option B) (m : M A) : M B :=
+Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
+    ∀ A, FinMapToList K A (M A)} {A B} (f : K → A → option B) (m : M A) : M B :=
   map_of_list (omap (λ ix, (fst ix,) <$> curry f ix) (map_to_list m)).
 
 (** * Theorems *)
@@ -124,25 +124,27 @@ Section setoid.
     - by intros m1 m2 ? i.
     - by intros m1 m2 m3 ?? i; trans (m2 !! i).
   Qed.
-  Global Instance lookup_proper (i: K) : Proper ((≡) ==> (≡)) (lookup (M:=M) i).
+  Global Instance lookup_proper (i : K) :
+    Proper ((≡) ==> (≡)) (lookup (M:=M A) i).
   Proof. by intros m1 m2 Hm. Qed.
   Global Instance partial_alter_proper :
-    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (partial_alter (M:=M)).
+    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (partial_alter (M:=M A)).
   Proof.
     by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
       rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne by done;
       try apply Hf; apply lookup_proper.
   Qed.
   Global Instance insert_proper (i : K) :
-    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=M) i).
+    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=M A) i).
   Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
-  Global Instance singleton_proper (i : K) :
-    Proper ((≡) ==> (≡)) (singletonM (M:=M) i).
+  Global Instance singleton_proper k :
+    Proper ((≡) ==> (≡)) (singletonM k : A → M A).
   Proof. by intros ???; apply insert_proper. Qed.
-  Global Instance delete_proper (i: K) : Proper ((≡) ==> (≡)) (delete (M:=M) i).
+  Global Instance delete_proper (i : K) :
+    Proper ((≡) ==> (≡)) (delete (M:=M A) i).
   Proof. by apply partial_alter_proper; [constructor|]. Qed.
   Global Instance alter_proper :
-    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (alter (M:=M)).
+    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (alter (A:=A) (M:=M A)).
   Proof.
     intros ?? Hf; apply partial_alter_proper.
     by destruct 1; constructor; apply Hf.
@@ -154,7 +156,7 @@ Section setoid.
     by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
   Qed.
   Global Instance union_with_proper :
-    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡)) (union_with (M:=M)).
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡)) (union_with (M:=M A)).
   Proof.
     intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
     by do 2 destruct 1; first [apply Hf | constructor].
diff --git a/theories/functions.v b/theories/functions.v
index a34f81fe97e55423e6a54dbc8896055c4858d909..ebc83e2d16f2e3bcb51bb6e346c3b37418d239d1 100644
--- a/theories/functions.v
+++ b/theories/functions.v
@@ -2,10 +2,10 @@ From stdpp Require Export base tactics.
 
 Section definitions.
   Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
-  Definition fn_insert (a : A) (t : T) (f : A → T) : A → T := λ b,
-    if decide (a = b) then t else f b.
-  Definition fn_alter (g : T → T) (a : A) (f : A → T) : A → T := λ b,
-    if decide (a = b) then g (f a) else f b.
+  Global Instance fn_insert : Insert A T (A → T) :=
+    λ a t f b, if decide (a = b) then t else f b.
+  Global Instance fn_alter : Alter A T (A → T) :=
+    λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b.
 End definitions.
 
 (* TODO: For now, we only have the properties here that do not need a notion
@@ -14,17 +14,17 @@ End definitions.
 Section functions.
   Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
 
-  Lemma fn_lookup_insert (f : A → T) a t : fn_insert a t f a = t.
-  Proof. unfold fn_insert. by destruct (decide (a = a)). Qed.
+  Lemma fn_lookup_insert (f : A → T) a t : <[a:=t]>f a = t.
+  Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed.
   Lemma fn_lookup_insert_rev  (f : A → T) a t1 t2 :
-    fn_insert a t1 f a = t2 → t1 = t2.
+    <[a:=t1]>f a = t2 → t1 = t2.
   Proof. rewrite fn_lookup_insert. congruence. Qed.
-  Lemma fn_lookup_insert_ne (f : A → T) a b t : a ≠ b → fn_insert a t f b = f b.
-  Proof. unfold fn_insert. by destruct (decide (a = b)). Qed.
+  Lemma fn_lookup_insert_ne (f : A → T) a b t : a ≠ b → <[a:=t]>f b = f b.
+  Proof. unfold insert, fn_insert. by destruct (decide (a = b)). Qed.
 
-  Lemma fn_lookup_alter (g : T → T) (f : A → T) a : fn_alter g a f a = g (f a).
-  Proof. unfold fn_alter. by destruct (decide (a = a)). Qed.
+  Lemma fn_lookup_alter (g : T → T) (f : A → T) a : alter g a f a = g (f a).
+  Proof. unfold alter, fn_alter. by destruct (decide (a = a)). Qed.
   Lemma fn_lookup_alter_ne (g : T → T) (f : A → T) a b :
-    a ≠ b → fn_alter g a f b = f b.
-  Proof. unfold fn_alter. by destruct (decide (a = b)). Qed.
+    a ≠ b → alter g a f b = f b.
+  Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
 End functions.
diff --git a/theories/gmap.v b/theories/gmap.v
index aa48152231b99494e874f16a6f3bfb404ddd3e41..88f62e36e4a4dff78a3cd68c564852288bd80b33 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -30,7 +30,7 @@ Proof.
 Defined.
 
 (** * Operations on the data structure *)
-Instance gmap_lookup `{Countable K} : Lookup K (gmap K) := λ A i m,
+Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
   let (m,_) := m in m !! encode i.
 Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
 Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i :
@@ -40,7 +40,8 @@ Proof.
   - rewrite decode_encode; eauto.
   - rewrite lookup_partial_alter_ne by done. by apply Hm.
 Qed.
-Instance gmap_partial_alter `{Countable K} : PartialAlter K (gmap K) := λ A f i m,
+Instance gmap_partial_alter `{Countable K} {A} :
+    PartialAlter K A (gmap K A) := λ f i m,
   let (m,Hm) := m in GMap (partial_alter f (encode i) m)
     (bool_decide_pack _ (gmap_partial_alter_wf f m i
     (bool_decide_unpack _ Hm))).
@@ -69,7 +70,7 @@ Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2,
   let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
   GMap (merge f' m1 m2) (bool_decide_pack _ (gmap_merge_wf f _ _
     (bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
-Instance gmap_to_list `{Countable K} : FinMapToList K (gmap K) := λ A m,
+Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
   let (m,_) := m in omap (λ ix : positive * A,
     let (i,x) := ix in (,x) <$> decode i) (map_to_list m).
 
@@ -113,7 +114,7 @@ Qed.
 
 (** * Finite sets *)
 Notation gset K := (mapset (gmap K)).
-Instance gset_dom `{Countable K} : Dom (gmap K) (gset K) := mapset_dom.
+Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
 Instance gset_dom_spec `{Countable K} :
   FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
diff --git a/theories/list.v b/theories/list.v
index 2608cebfbb5dc933d7d283b422b788b108c0514a..59b7bda9e163ca67ae0ac65fc67e7cb712b78b87 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -57,15 +57,15 @@ Existing Instance list_equiv.
 
 (** The operation [l !! i] gives the [i]th element of the list [l], or [None]
 in case [i] is out of bounds. *)
-Instance list_lookup : Lookup nat list :=
-  fix go A i l {struct l} : option A := let _ : Lookup _ _ := @go in
+Instance list_lookup {A} : Lookup nat A (list A) :=
+  fix go i l {struct l} : option A := let _ : Lookup _ _ _ := @go in
   match l with
   | [] => None | x :: l => match i with 0 => Some x | S i => l !! i end
   end.
 
 (** The operation [alter f i l] applies the function [f] to the [i]th element
 of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
-Instance list_alter : Alter nat list := λ A f,
+Instance list_alter {A} : Alter nat A (list A) := λ f,
   fix go i l {struct l} :=
   match l with
   | [] => []
@@ -74,8 +74,8 @@ Instance list_alter : Alter nat list := λ A f,
 
 (** The operation [<[i:=x]> l] overwrites the element at position [i] with the
 value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
-Instance list_insert : Insert nat list :=
-  fix go A i y l {struct l} := let _ : Insert _ _ := @go in
+Instance list_insert {A} : Insert nat A (list A) :=
+  fix go i y l {struct l} := let _ : Insert _ _ _ := @go in
   match l with
   | [] => []
   | x :: l => match i with 0 => y :: l | S i => x :: <[i:=y]>l end
@@ -90,11 +90,11 @@ Instance: Params (@list_inserts) 1.
 (** The operation [delete i l] removes the [i]th element of [l] and moves
 all consecutive elements one position ahead. In case [i] is out of bounds,
 the list is returned unchanged. *)
-Instance list_delete : Delete nat list :=
-  fix go A (i : nat) (l : list A) {struct l} : list A :=
+Instance list_delete {A} : Delete nat (list A) :=
+  fix go (i : nat) (l : list A) {struct l} : list A :=
   match l with
   | [] => []
-  | x :: l => match i with 0 => l | S i => x :: @delete _ _ go _ i l end
+  | x :: l => match i with 0 => l | S i => x :: @delete _ _ go i l end
   end.
 
 (** The function [option_list o] converts an element [Some x] into the
@@ -2733,13 +2733,13 @@ Section setoid.
   Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n).
   Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_lookup_proper i :
-    Proper ((≡) ==> (≡)) (lookup (M:=list) i).
+    Proper ((≡) ==> (≡)) (lookup (M:=list A) i).
   Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed.
   Global Instance list_alter_proper f i :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list) f i).
+    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
   Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
   Global Instance list_insert_proper i :
-    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list) i).
+    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) i).
   Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
   Global Instance list_inserts_proper i :
     Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i).
@@ -2748,7 +2748,7 @@ Section setoid.
     induction Hk; intros ????; simpl; try f_equiv; naive_solver.
   Qed.
   Global Instance list_delete_proper i :
-    Proper ((≡) ==> (≡)) (delete (M:=list) i).
+    Proper ((≡) ==> (≡)) (delete (M:=list A) i).
   Proof. induction i; destruct 1; try constructor; eauto. Qed.
   Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A).
   Proof. destruct 1; by constructor. Qed.
diff --git a/theories/mapset.v b/theories/mapset.v
index 2ecdf0e24ff93363486ab76e3b4776add8c31607..b75e6140f5bc76e5c6bba672f10caa291650cce3 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -118,7 +118,7 @@ Proof.
   - destruct (Is_true_reflect (f a)); naive_solver.
   - naive_solver.
 Qed.
-Instance mapset_dom : Dom M (mapset M) := λ A, mapset_dom_with (λ _, true).
+Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
 Instance mapset_dom_spec: FinMapDom K M (mapset M).
 Proof.
   split; try apply _. intros. unfold dom, mapset_dom, is_Some.
diff --git a/theories/natmap.v b/theories/natmap.v
index 600fbce1cd7b8869c1483d23355a758e4c56e36f..9c7e89952cbd461ea895bb67d7a8a67359fb38f1 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -44,7 +44,7 @@ Global Instance natmap_eq_dec `{∀ x y : A, Decision (x = y)}
   end.
 
 Instance natmap_empty {A} : Empty (natmap A) := NatMap [] I.
-Instance natmap_lookup : Lookup nat natmap := λ A i m,
+Instance natmap_lookup {A} : Lookup nat A (natmap A) := λ i m,
   let (l,_) := m in mjoin (l !! i).
 
 Fixpoint natmap_singleton_raw {A} (i : nat) (x : A) : natmap_raw A :=
@@ -92,7 +92,7 @@ Proof.
   revert i. induction l; [intro | intros [|?]]; simpl; repeat case_match;
     eauto using natmap_singleton_wf, natmap_cons_canon_wf, natmap_wf_inv.
 Qed.
-Instance natmap_alter : PartialAlter nat natmap := λ A f i m,
+Instance natmap_alter {A} : PartialAlter nat A (natmap A) := λ f i m,
   let (l,Hl) := m in NatMap _ (natmap_alter_wf f i l Hl).
 Lemma natmap_lookup_alter_raw {A} (f : option A → option A) i l :
   mjoin (natmap_alter_raw f i l !! i) = f (mjoin (l !! i)).
@@ -188,7 +188,7 @@ Proof.
   revert i. induction l as [|[?|] ? IH]; simpl; try constructor; auto.
   rewrite natmap_elem_of_to_list_raw_aux. intros (?&?&?). lia.
 Qed.
-Instance natmap_to_list : FinMapToList nat natmap := λ A m,
+Instance natmap_to_list {A} : FinMapToList nat A (natmap A) := λ m,
   let (l,_) := m in natmap_to_list_raw 0 l.
 
 Definition natmap_map_raw {A B} (f : A → B) : natmap_raw A → natmap_raw B :=
@@ -256,7 +256,7 @@ Qed.
 
 (** Finally, we can construct sets of [nat]s satisfying extensional equality. *)
 Notation natset := (mapset natmap).
-Instance natmap_dom : Dom natmap natset := mapset_dom.
+Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
 Instance: FinMapDom nat natmap natset := mapset_dom_spec.
 
 (* Fixpoint avoids this definition from being unfolded *)
diff --git a/theories/nmap.v b/theories/nmap.v
index 9d56d9c835adbc84e7e2600ac9bd4a908ef5e2f0..c839a659b43d616f38e6518154e87479f7999801 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -22,17 +22,17 @@ Proof.
 Defined.
 Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
 Global Opaque Nempty.
-Instance Nlookup : Lookup N Nmap := λ A i t,
+Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
   match i with
   | N0 => Nmap_0 t
   | Npos p => Nmap_pos t !! p
   end.
-Instance Npartial_alter : PartialAlter N Nmap := λ A f i t,
+Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
   match i, t with
   | N0, NMap o t => NMap (f o) t
   | Npos p, NMap o t => NMap o (partial_alter f p t)
   end.
-Instance Nto_list : FinMapToList N Nmap := λ A t,
+Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
   match t with
   | NMap o t =>
      default [] o (λ x, [(0,x)]) ++ (prod_map Npos id <$> map_to_list t)
@@ -82,7 +82,7 @@ Qed.
 (** * Finite sets *)
 (** We construct sets of [N]s satisfying extensional equality. *)
 Notation Nset := (mapset Nmap).
-Instance Nmap_dom : Dom Nmap Nset := mapset_dom.
+Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
 Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
 
 (** * Fresh numbers *)
diff --git a/theories/option.v b/theories/option.v
index cefc66683141de8eb34e38e5d52727e053b7d257..5af4b5a039438871f4996114956b1acd1153b071 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -239,16 +239,16 @@ Instance maybe_Some {A} : Maybe (@Some A) := id.
 Arguments maybe_Some _ !_ /.
 
 (** * Union, intersection and difference *)
-Instance option_union_with : UnionWith option := λ A f mx my,
+Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
   match mx, my with
   | Some x, Some y => f x y
   | Some x, None => Some x
   | None, Some y => Some y
   | None, None => None
   end.
-Instance option_intersection_with : IntersectionWith option := λ A f mx my,
-  match mx, my with Some x, Some y => f x y | _, _ => None end.
-Instance option_difference_with : DifferenceWith option := λ A f mx my,
+Instance option_intersection_with {A} : IntersectionWith A (option A) :=
+  λ f mx my, match mx, my with Some x, Some y => f x y | _, _ => None end.
+Instance option_difference_with {A} : DifferenceWith A (option A) := λ f mx my,
   match mx, my with
   | Some x, Some y => f x y
   | Some x, None => Some x
diff --git a/theories/pmap.v b/theories/pmap.v
index 5dcfcafec09b3576e1f774dcadaf1e11aa3f5a44..38ee622698c5cd254ce994ca6bab91ea4de081e6 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -52,9 +52,9 @@ Local Hint Resolve PNode_wf.
 
 (** Operations *)
 Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
-Instance Plookup_raw : Lookup positive Pmap_raw :=
-  fix go A (i : positive) (t : Pmap_raw A) {struct t} : option A :=
-  let _ : Lookup _ _ := @go in
+Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
+  fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
+  let _ : Lookup _ _ _ := @go in
   match t with
   | PLeaf => None
   | PNode o l r => match i with 1 => o | i~0 => l !! i | i~1 => r !! i end
@@ -273,12 +273,12 @@ Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)}
   | right H => right (H ∘ proj1 (Pmap_eq m1 m2))
   end.
 Instance Pempty {A} : Empty (Pmap A) := PMap ∅ I.
-Instance Plookup : Lookup positive Pmap := λ A i m, pmap_car m !! i.
-Instance Ppartial_alter : PartialAlter positive Pmap := λ A f i m,
+Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
+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).
 Instance Pfmap : FMap Pmap := λ A B f m,
   let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
-Instance Pto_list : FinMapToList positive Pmap := λ A m,
+Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
   let (t,Ht) := m in Pto_list_raw 1 t [].
 Instance Pomap : OMap Pmap := λ A B f m,
   let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
@@ -305,7 +305,7 @@ Qed.
 (** * Finite sets *)
 (** We construct sets of [positives]s satisfying extensional equality. *)
 Notation Pset := (mapset Pmap).
-Instance Pmap_dom : Dom Pmap Pset := mapset_dom.
+Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
 Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
 
 (** * Fresh numbers *)
diff --git a/theories/zmap.v b/theories/zmap.v
index 7ead0d0299b541895335ac8f2bdc23791ad046e4..a0644bfa58e9214aa9b67ab7db170574b0d0de8f 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -23,17 +23,17 @@ Proof.
   end; abstract congruence.
 Defined.
 Instance Zempty {A} : Empty (Zmap A) := ZMap None ∅ ∅.
-Instance Zlookup : Lookup Z Zmap := λ A i t,
+Instance Zlookup {A} : Lookup Z A (Zmap A) := λ i t,
   match i with
   | Z0 => Zmap_0 t | Zpos p => Zmap_pos t !! p | Zneg p => Zmap_neg t !! p
   end.
-Instance Zpartial_alter : PartialAlter Z Zmap := λ A f i t,
+Instance Zpartial_alter {A} : PartialAlter Z A (Zmap A) := λ f i t,
   match i, t with
   | Z0, ZMap o t t' => ZMap (f o) t t'
   | Zpos p, ZMap o t t' => ZMap o (partial_alter f p t) t'
   | Zneg p, ZMap o t t' => ZMap o t (partial_alter f p t')
   end.
-Instance Zto_list : FinMapToList Z Zmap := λ A t,
+Instance Zto_list {A} : FinMapToList Z A (Zmap A) := λ t,
   match t with
   | ZMap o t t' => default [] o (λ x, [(0,x)]) ++
      (prod_map Zpos id <$> map_to_list t) ++
@@ -93,5 +93,5 @@ Qed.
 (** * Finite sets *)
 (** We construct sets of [Z]s satisfying extensional equality. *)
 Notation Zset := (mapset Zmap).
-Instance Zmap_dom : Dom Zmap Zset := mapset_dom.
+Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
 Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.