From d3e1e7ff70723be3ec294b29ebbdb9c6ac7b313e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Mar 2021 14:00:28 +0100
Subject: [PATCH] explicitly note that we are quantifying over an Iris goal
 here

---
 iris/program_logic/adequacy.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 199e6aef4..d9340a5cc 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -125,6 +125,8 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
          (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
          (Φs : list (val Λ → iProp Σ))
          (fork_post : val Λ → iProp Σ)
+         (* Note: existentially quantifying over Iris goal! [iExists _] should
+         usually work. *)
          state_interp_mono,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
                                   state_interp_mono
-- 
GitLab