From 045c820306081549f8e3e3d7f5f7b69d317496ff Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Nov 2019 11:24:03 +0100
Subject: [PATCH] Bump Iris (`iPoseProof` changes).

---
 opam                                          | 2 +-
 theories/experimental/helping/helping_stack.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam b/opam
index 193e3a0..0a7b23a 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2019-11-07.1.891124d6") | (= "dev") }
+  "coq-iris" { (= "dev.2019-11-21.0.e0d10c05") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index 376e0f9..35fcf2f 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -613,7 +613,7 @@ Section refinement.
     rel_alloc_l st as "Hst". rel_pure_l. rel_pure_l. rel_pure_l. rel_pure_l.
     iMod (own_alloc (● to_offer_reg ∅ : authR offerRegR)) as (γo) "Hor".
     { apply auth_auth_valid. apply to_offer_reg_valid. }
-    iMod (inv_alloc stackN _ (stackInv _ γo st st' mb lk) with "[-]") as "#Hinv".
+    iMod (inv_alloc stackN _ (stackInv A γo st st' mb lk) with "[-]") as "#Hinv".
     { iNext. unfold stackInv.
       iExists None, _, _. iFrame.
       iSplit; eauto.
-- 
GitLab