diff --git a/opam b/opam
index 193e3a075eb0708627f9799779dac21770540aa9..0a7b23a3f36582050c475404635f51f33c3b3576 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 376e0f9847cb262a4af763406a23fa422c108cc3..35fcf2f4ccee2c21a0145448ea4d5308be02390a 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.