From 2581dc19411bbf14b683336cfe4cb91ee7e93532 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Mar 2019 07:02:18 +0100
Subject: [PATCH] Bump stdpp.

---
 opam                    | 2 +-
 theories/algebra/gmap.v | 2 +-
 theories/algebra/gset.v | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/opam b/opam
index 703b2fe66..9c08e8799 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 1f402b14e..018ae8697 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 ee2c85116..380c874b8 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.
-- 
GitLab