From 1ca7f402281bc3822e94f7444f6edf774fd7e548 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 Aug 2022 17:37:47 -0400
Subject: [PATCH] update dependencies
---
coq-gpfsl.opam | 4 ++--
theories/base_logic/adequacy.v | 2 +-
theories/base_logic/history.v | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index d82c21a0..11843468 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,8 +10,8 @@ version: "dev"
synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
depends: [
- "coq-iris" { (= "dev.2022-07-27.1.d01b4bc8") | (= "dev") }
- "coq-orc11" { (= "dev.2022-07-27.0.cadba960") | (= "dev") }
+ "coq-iris" { (= "dev.2022-08-03.0.949ab7bc") | (= "dev") }
+ "coq-orc11" { (= "dev.2022-07-30.0.e76351a5") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/base_logic/adequacy.v b/theories/base_logic/adequacy.v
index 9619f3e0..23e27bf6 100644
--- a/theories/base_logic/adequacy.v
+++ b/theories/base_logic/adequacy.v
@@ -55,7 +55,7 @@ Lemma noprol_adequacy Σ `{!noprolGpreS Σ} e (σ : state) 𝓥 φ :
Proof.
(* TODO: we cannot use [ownP_adequacy] because it fixes a state_interp. We
have to embed [ownP_adequacy]'s proof here instead. *)
- intros WFσ H𝓥 Hwp; eapply (wp_adequacy_lc _ _); iIntros (Hinv ??).
+ intros WFσ H𝓥 Hwp; eapply (wp_adequacy _ _); iIntros (Hinv ?).
set (M := mem_cut σ.(mem) σ.(na)).
iMod (gen_heap_init (to_hist M)) as (HEAPG) "(Hist & hists & metas)".
iMod (own_alloc (● (∅ : hist_freeableUR))) as (hist_freeable_name) "hf".
diff --git a/theories/base_logic/history.v b/theories/base_logic/history.v
index cc8bdec1..03e79f0c 100644
--- a/theories/base_logic/history.v
+++ b/theories/base_logic/history.v
@@ -170,7 +170,7 @@ Definition hist_inv_content `{!noprolG Σ} : iProp Σ :=
Definition histN : namespace := nroot .@ "history".
Definition hist_inv `{!noprolG Σ} : iProp Σ :=
- @inv _ (ownP_invG) histN hist_inv_content.
+ @inv _ _ (ownP_invG) histN hist_inv_content.
Definition hist_interp `{!noprolG Σ} σ : iProp Σ :=
(own ownP_name (●E σ) ∗ hist_inv)%I.
--
GitLab