From c2eaa77dc1d42edb09e8ed0c1cab290b23a292bf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Jul 2019 19:19:06 +0200
Subject: [PATCH] dont quantify over empty telescopes

---
 theories/program_logic/atomic.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 487acd356..847f2705c 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -112,8 +112,8 @@ Section lemmas.
   (* Sequential triples with a persistent precondition and no initial quantifier
   are atomic. *)
   Lemma seq_wp_atomic e Eo (α : [tele] → iProp) (β : [tele] → TB → iProp)
-        (f : [tele] → TB → val Λ) {HP : ∀.. x, Persistent (α x)} :
-    (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}) -∗
+        (f : [tele] → TB → val Λ) {HP : Persistent (α [tele_arg])} :
+    (∀ Φ, α [tele_arg] -∗ (∀.. y, β [tele_arg] y -∗ Φ (f [tele_arg] y)) -∗ WP e {{ Φ }}) -∗
     atomic_wp e Eo α β f.
   Proof.
     simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.
-- 
GitLab