diff --git a/opam b/opam
index bb7f1ad481d690c9612be5f40a923e07f35a2b96..1f1cc0596dd4c1dbc8221f4ee846e0de230db0f2 100644
--- a/opam
+++ b/opam
@@ -12,5 +12,5 @@ remove: ["sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'"]
 depends: [
   "coq" { >= "8.6.1" & < "8.8~" }
   "coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2017-09-20.2") | (= "dev") }
+  "coq-stdpp" { (= "2017-09-21.2") | (= "dev") }
 ]
diff --git a/opam.pins b/opam.pins
index 434e1768082f3e51969c3931fbac76433aa919fc..7034b445798280e7b05ccc6b0c8caa5190eef4b8 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 9b0f7c75a2387e0ad9fe5d16ec1083a0ece2bea3
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 2f9f3d3f28aa568f5cbee1be5699f163800491c0
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index 73be6c2815ed300d73dcc2e4ce7eeb5f92027719..e8354972a5cc90864c1a9395f2f5d529eb96b845 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -180,11 +180,11 @@ Section gmap.
 
   Global Instance big_opM_ne n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> eq ==> dist n)
-           (big_opM o (A:=A)).
+           (big_opM o (K:=K) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
   Global Instance big_opM_proper' :
     Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> eq ==> (≡))
-           (big_opM o (A:=A)).
+           (big_opM o (K:=K) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_opM_empty f : ([^o map] k↦x ∈ ∅, f k x) = monoid_unit.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 7513358c697b7df2b27e22896288527a9bfc3f29..932aa37218504f1a47c634a095dd5f998eaa7b68 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -427,7 +427,7 @@ Lemma singleton_local_update m i x y x' y' :
   (m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}).
 Proof.
   intros. rewrite /singletonM /map_singleton -(insert_insert ∅ i y' y).
-  eapply insert_local_update; eauto using lookup_insert.
+  by eapply insert_local_update; [|eapply lookup_insert|].
 Qed.
 
 Lemma delete_local_update m1 m2 i x `{!Exclusive x} :
@@ -446,7 +446,7 @@ Lemma delete_singleton_local_update m i x `{!Exclusive x} :
   (m, {[ i := x ]}) ~l~> (delete i m, ∅).
 Proof.
   rewrite -(delete_singleton i x).
-  eapply delete_local_update; eauto using lookup_singleton.
+  by eapply delete_local_update, lookup_singleton.
 Qed.
 
 Lemma delete_local_update_cancelable m1 m2 i mx `{!Cancelable mx} :
diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 9012d629c0e9d82d03641b56e05bf402c7a27d63..9b9daea32a22a5a4ff0b6ca3b520d6d444b436e9 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -213,7 +213,7 @@ Section gmap.
 
   Global Instance big_sepM_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
-           (big_opM (@uPred_sep M) (A:=A)).
+           (big_opM (@uPred_sep M) (K:=K) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
 
   Lemma big_sepM_empty Φ : ([∗ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 79e199df2a8b17881d51595c110545faf1d79e5b..89914dc635f5dbd3fd2bf3e94a2c61cae981e9ae 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -15,6 +15,7 @@ Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
   gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
   gen_heap_name : gname
 }.
+Arguments gen_heap_name {_ _ _ _ _} _ : assert.
 
 Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
   { gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
@@ -27,13 +28,13 @@ Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
 Proof. solve_inG. Qed.
 
 Section definitions.
-  Context `{gen_heapG L V Σ}.
+  Context `{hG : gen_heapG L V Σ}.
 
   Definition gen_heap_ctx (σ : gmap L V) : iProp Σ :=
-    own gen_heap_name (● to_gen_heap σ).
+    own (gen_heap_name hG) (● (to_gen_heap σ)).
 
   Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
-    own gen_heap_name (â—¯ {[ l := (q, to_agree (v : leibnizC V)) ]}).
+    own (gen_heap_name hG) (â—¯ {[ l := (q, to_agree (v : leibnizC V)) ]}).
   Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
   Definition mapsto := unseal mapsto_aux.
   Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
@@ -77,6 +78,8 @@ Section gen_heap.
   Implicit Types Φ : V → iProp Σ.
   Implicit Types σ : gmap L V.
   Implicit Types h g : gen_heapUR L V.
+  Implicit Types l : L.
+  Implicit Types v : V.
 
   (** General properties of mapsto *)
   Global Instance mapsto_timeless l q v : TimelessP (l ↦{q} v).
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 3e88d0de64648c589530fd4b86f2b365cfc0f52b..bb3a90d309e74219f479b2295e02f93fa48597c6 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -394,7 +394,7 @@ Qed.
 Lemma alloc_fresh e v σ :
   let l := fresh (dom (gset loc) σ) in
   to_val e = Some v → head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
-Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
+Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
 
 (* Misc *)
 Lemma to_val_rec f x e `{!Closed (f :b: x :b: []) e} :