From 152eaab993ca22157186c991f92d6a71fe47a549 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <gaeher@mpi-sws.org>
Date: Wed, 30 Nov 2022 09:16:08 +0100
Subject: [PATCH] bump iris
---
semantics.opam | 2 +-
theories/program_logics/program_logic/adequacy.v | 1 +
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/semantics.opam b/semantics.opam
index 6324efb..19d4d90 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -10,7 +10,7 @@ version: "dev"
depends: [
"coq" { (>= "8.13" & < "8.17~") | (= "dev") }
- "coq-iris-heap-lang" { (= "dev.2022-11-24.2.5b5d3f4d") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2022-11-29.2.de908f52") | (= "dev") }
"coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15") | (= "1.3+8.16") }
"coq-autosubst" { (= "1.7") | (= "dev") }
]
diff --git a/theories/program_logics/program_logic/adequacy.v b/theories/program_logics/program_logic/adequacy.v
index 07c035e..499558f 100644
--- a/theories/program_logics/program_logic/adequacy.v
+++ b/theories/program_logics/program_logic/adequacy.v
@@ -145,6 +145,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invGpreS Σ} e σ1 n κs t2 σ2 φ :
φ.
Proof.
intros Hwp ?.
+ eapply pure_soundness.
apply (step_fupdN_soundness_no_lc _ n 0)=> Hinv.
iIntros "_".
iMod Hwp as (s stateI Φ) "(Hσ & Hwp & Hφ)".
--
GitLab