diff --git a/opam b/opam
index 703b2fe663ad6f9398ddfce854ab7c4885e1af0b..9c08e879969128bd606c46d958ede293d5a6cd5c 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2019-02-22.0.45ae06c7") | (= "dev") }
+  "coq-stdpp" { (= "dev.2019-03-03.0.7b80dd85") | (= "dev") }
 ]
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 1f402b14e525bee08c6b98ee50ad4740a72ce031..018ae86979bb83a8c9caa946c8b37823429273df 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -353,7 +353,7 @@ Qed.
 
 Section freshness.
   Local Set Default Proof Using "Type*".
-  Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
+  Context `{Infinite K}.
   Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
     ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
   Proof.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index ee2c85116b908ad26418a3e8cb9e47d8656f4584..380c874b88be0a4abfd3d4e5264aefada85c0a2f 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -163,13 +163,13 @@ Section gset_disj.
 
   Section fresh_updates.
     Local Set Default Proof Using "Type*".
-    Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
+    Context `{Infinite K}.
 
     Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X :
       (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
     Proof.
       intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto.
-      intros Y ?; exists (fresh Y); eauto using is_fresh.
+      intros Y ?; exists (fresh Y). split. apply is_fresh. done.
     Qed.
     Lemma gset_disj_alloc_updateP' X :
       GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.