From 56e9d264c7ecbebfd209a0048159c12781a8a53d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 17 May 2022 11:34:01 +0200
Subject: [PATCH] cleanup imports

---
 tests/atomic.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/atomic.v b/tests/atomic.v
index e00a871bc..114ccd8cc 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,6 +1,4 @@
-Require Import stdpp.coPset.
-Require Import iris.bi.telescopes.
-Require Import iris.bi.lib.atomic.
+From iris.bi Require Import atomic.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
@@ -11,6 +9,8 @@ Unset Mangle Names.
 Section definition.
   Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
 
+  (** We can quantify over telescopes *inside* Iris and use them with atomic
+  updates. *)
   Definition AU_tele_quantify_iris : Prop :=
     ⊢ ∀ (TA TB : tele) (α : TA → PROP) (β Φ : TA → TB → PROP),
         atomic_update Eo Ei α β Φ.
-- 
GitLab