diff --git a/opam b/opam
index 1fc1d3a78c856b3ca96cecf203a5030ef1c5cbcc..a8ce3bbe3d34bbb83bf5a48ecfccb955fe6361b6 100644
--- a/opam
+++ b/opam
@@ -12,5 +12,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2019-08-24.1.adfc24d2") | (= "dev") }
+  "coq-stdpp" { (= "dev.2019-08-26.0.1ae85171") | (= "dev") }
 ]
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 714b01afb9e2cf23298daa6c8a6456a6e3fd2839..635bb926744c54f3872d50f0857699cd07e55e0d 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -971,6 +971,24 @@ Section unit.
   Proof. by constructor. Qed.
 End unit.
 
+(** ** CMRA for the empty type *)
+Section empty.
+  Instance Empty_set_valid : Valid Empty_set := λ x, False.
+  Instance Empty_set_validN : ValidN Empty_set := λ n x, False.
+  Instance Empty_set_pcore : PCore Empty_set := λ x, Some x.
+  Instance Empty_set_op : Op Empty_set := λ x y, x.
+  Lemma Empty_set_cmra_mixin : CmraMixin Empty_set.
+  Proof. apply discrete_cmra_mixin, ra_total_mixin; by (intros [] || done). Qed.
+  Canonical Structure Empty_setR : cmraT := CmraT Empty_set Empty_set_cmra_mixin.
+
+  Global Instance Empty_set_cmra_discrete : CmraDiscrete Empty_setR.
+  Proof. done. Qed.
+  Global Instance Empty_set_core_id (x : Empty_set) : CoreId x.
+  Proof. by constructor. Qed.
+  Global Instance Empty_set_cancelable (x : Empty_set) : Cancelable x.
+  Proof. by constructor. Qed.
+End empty.
+
 (** ** Natural numbers *)
 Section nat.
   Instance nat_valid : Valid nat := λ x, True.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1f53c8d72bdc098e3d6bdc53b44b4ae18097793f..e8b30026792340750f5dbd320dd3e042b0569643 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -616,6 +616,20 @@ Section unit.
   Proof. done. Qed.
 End unit.
 
+(** empty *)
+Section empty.
+  Instance Empty_set_dist : Dist Empty_set := λ _ _ _, True.
+  Definition Empty_set_ofe_mixin : OfeMixin Empty_set.
+  Proof. by repeat split; try exists 0. Qed.
+  Canonical Structure Empty_setO : ofeT := OfeT Empty_set Empty_set_ofe_mixin.
+
+  Global Program Instance Empty_set_cofe : Cofe Empty_setO := { compl x := x 0 }.
+  Next Obligation. by repeat split; try exists 0. Qed.
+
+  Global Instance Empty_set_ofe_discrete : OfeDiscrete Empty_setO.
+  Proof. done. Qed.
+End empty.
+
 (** Product *)
 Section product.
   Context {A B : ofeT}.