From e60de03fe711e3b0c21fcef0de947ce6824f90fd Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 16 May 2022 23:12:33 +0200
Subject: [PATCH 1/2] Bump stdpp for universe fix

---
 coq-iris.opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq-iris.opam b/coq-iris.opam
index 5b1248bcc..e956a53c9 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2022-05-13.2.8b17ca72") | (= "dev") }
+  "coq-stdpp" { (= "dev.2022-05-16.1.411eb445") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
-- 
GitLab


From 9851ef8d54db20ea5f84e544160721e325927d89 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 16 May 2022 12:55:35 +0200
Subject: [PATCH 2/2] Add testcase for #461

---
 tests/atomic.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/tests/atomic.v b/tests/atomic.v
index fc69d02d0..e00a871bc 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,3 +1,6 @@
+Require Import stdpp.coPset.
+Require Import iris.bi.telescopes.
+Require Import iris.bi.lib.atomic.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
@@ -5,6 +8,14 @@ From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
+Section definition.
+  Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
+
+  Definition AU_tele_quantify_iris : Prop :=
+    ⊢ ∀ (TA TB : tele) (α : TA → PROP) (β Φ : TA → TB → PROP),
+        atomic_update Eo Ei α β Φ.
+End definition.
+
 Section tests.
   Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
   Import atomic_heap.notation.
-- 
GitLab