Bump stdpp.

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") }
 ]

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.

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.