Bump Iris (iExists ?).

opam

@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
 synopsis: "A collection of case studies for Iris"
 
 depends: [
-  "coq-iris" { (= "dev.2020-07-15.7.fa9d6a7c") | (= "dev") }
+  "coq-iris" { (= "dev.2020-07-21.0.e4347ec2") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
   "coq-iris-string-ident"
 ]

theories/concurrent_stacks/concurrent_stack4.v

@@ -240,13 +240,13 @@ Section proofs.
       wp_pures.
       wp_apply (revoke_works with "[Hrev]"); first auto.
       iIntros (v') "H"; iApply "HΦ"; auto.
-    - iDestruct "Hsome" as (? ? ?) "[Hl _]". wp_store.
+    - iDestruct "Hsome" as (v' γ' Q') "[Hl _]". wp_store.
       iMod ("Hclose" with "[Hl]") as "_".
       { iNext; iRight; iExists _, _, _; by iFrame. }
       iModIntro.
       wp_pures.
       wp_apply (revoke_works with "[Hrev]"); first auto.
-      iIntros (v') "H"; iApply "HΦ"; auto.
+      iIntros (v'') "H"; iApply "HΦ"; auto.
   Qed.
 
   Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I