From 86460eea396e6bc2f0a7869fdbd26c2974f90e9e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 13 Jun 2019 06:51:29 +0200
Subject: [PATCH] Bump Iris.

---
 opam                                             | 2 +-
 theories/logrel/F_mu/soundness.v                 | 2 +-
 theories/logrel/F_mu_ref/soundness.v             | 2 +-
 theories/logrel/F_mu_ref/soundness_binary.v      | 2 +-
 theories/logrel/F_mu_ref_conc/soundness_binary.v | 2 +-
 theories/logrel/F_mu_ref_conc/soundness_unary.v  | 2 +-
 theories/logrel/stlc/soundness.v                 | 2 +-
 7 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/opam b/opam
index ec4e7bc..e8fe5ce 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2019-06-11.8.a51fa3cf") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-12.4.ae1dd418") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/logrel/F_mu/soundness.v b/theories/logrel/F_mu/soundness.v
index ade3e7d..ce7b3fb 100644
--- a/theories/logrel/F_mu/soundness.v
+++ b/theories/logrel/F_mu/soundness.v
@@ -9,7 +9,7 @@ Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
 Proof.
   intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
   eapply (wp_adequacy Σ); eauto.
-  iIntros (Hinv ?). iModIntro. iExists (λ _ _, True%I). iSplit=> //.
+  iIntros (Hinv ?). iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=> //.
   replace e with e.[env_subst[]] by by asimpl.
   set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
   iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto.
diff --git a/theories/logrel/F_mu_ref/soundness.v b/theories/logrel/F_mu_ref/soundness.v
index f75f231..fff5f5a 100644
--- a/theories/logrel/F_mu_ref/soundness.v
+++ b/theories/logrel/F_mu_ref/soundness.v
@@ -17,7 +17,7 @@ Proof.
   eapply (wp_adequacy Σ _); eauto.
   iIntros (Hinv ?).
   iMod (gen_heap_init σ) as (Hheap) "Hh".
-  iModIntro. iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  iModIntro. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
   set (HeapΣ := (HeapG Σ Hinv Hheap)).
   iApply (wp_wand with "[]").
   - replace e with e.[env_subst[]] by by asimpl.
diff --git a/theories/logrel/F_mu_ref/soundness_binary.v b/theories/logrel/F_mu_ref/soundness_binary.v
index 00bbf0c..b16a847 100644
--- a/theories/logrel/F_mu_ref/soundness_binary.v
+++ b/theories/logrel/F_mu_ref/soundness_binary.v
@@ -25,7 +25,7 @@ Proof.
     rewrite /to_gen_heap fin_maps.map_fmap_empty.
     iFrame. }
   set (HeapΣ := HeapG Σ Hinv Hheap).
-  iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
   iApply wp_fupd. iApply (wp_wand with "[-]").
   - iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel".
     { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
diff --git a/theories/logrel/F_mu_ref_conc/soundness_binary.v b/theories/logrel/F_mu_ref_conc/soundness_binary.v
index bf10c67..d747ae1 100644
--- a/theories/logrel/F_mu_ref_conc/soundness_binary.v
+++ b/theories/logrel/F_mu_ref_conc/soundness_binary.v
@@ -22,7 +22,7 @@ Proof.
   iMod (inv_alloc specN _ (spec_inv ([e'], ∅)) with "[Hcfg1]") as "#Hcfg".
   { iNext. iExists [e'], ∅. rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
   set (HeapΣ := (HeapIG Σ Hinv Hheap)).
-  iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
   iApply wp_fupd. iApply wp_wand_r.
   iSplitL.
   iPoseProof ((Hlog _ _ [] []) with "[]") as "Hrel".
diff --git a/theories/logrel/F_mu_ref_conc/soundness_unary.v b/theories/logrel/F_mu_ref_conc/soundness_unary.v
index 7a1213f..c122efa 100644
--- a/theories/logrel/F_mu_ref_conc/soundness_unary.v
+++ b/theories/logrel/F_mu_ref_conc/soundness_unary.v
@@ -16,7 +16,7 @@ Proof.
   intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
   eapply (wp_adequacy Σ _). iIntros (Hinv ?).
   iMod (gen_heap_init σ) as (Hheap) "Hh".
-  iModIntro. iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  iModIntro. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
   set (HeapΣ := (HeapIG Σ Hinv Hheap)).
   iApply (wp_wand with "[]").
   - replace e with e.[env_subst[]] by by asimpl.
diff --git a/theories/logrel/stlc/soundness.v b/theories/logrel/stlc/soundness.v
index be359de..d080562 100644
--- a/theories/logrel/stlc/soundness.v
+++ b/theories/logrel/stlc/soundness.v
@@ -16,7 +16,7 @@ Proof.
   set (Σ := invΣ). intros.
   cut (adequate NotStuck e () (λ _ _, True)); first (intros [_ Hsafe]; eauto).
   eapply (wp_adequacy Σ _). iIntros (Hinv ?).
-  iModIntro. iExists (λ _ _, True%I). iSplit=>//.
+  iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=>//.
   set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
   iApply (wp_wand with "[]"). by iApply wp_soundness. eauto.
 Qed.
-- 
GitLab