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] 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