update iris

refinedc.opam

@@ -17,7 +17,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
 
 depends: [
   "coq" { (>= "8.12.0" & < "8.13~") }
-  "coq-iris" { (= "dev.2020-11-12.3.126531ec") | (= "dev") }
+  "coq-iris" { (= "dev.2020-12-06.1.7dada503") | (= "dev") }
   "dune" {>= "2.7.0"}
   "cerberus" {= "~dev"}
   "cmdliner" {>= "1.0.4"}

theories/lang/lifting.v

@@ -434,7 +434,7 @@ Lemma wps_bind Q Ψ Ks e E:
 Proof.
   iIntros "He". iLöb as "IH" forall (e).
   move Hv: (to_val e) => [|]. {
-    move => /of_to_val <-. iApply fupd_wps. by iMod (wp_value_inv' with "He").
+    move => /of_to_val <-. rewrite wp_value_fupd'. by iApply fupd_wps.
   }
   iApply wps_lift_stmt_step.
   iIntros (?? ->). iSplit. {

theories/lang/proofmode.v

@@ -34,7 +34,7 @@ Lemma tac_wp_bind' `{refinedcG Σ} e Ks Φ E:
 Proof.
   move: Ks Φ => /=. elim/rev_ind. {
     iIntros (Φ) "He". iApply @wp_fupd.
-    iApply (wp_wand with "He") => /=. iIntros (v). iApply @wp_value_inv'.
+    iApply (wp_wand with "He") => /=. iIntros (v). rewrite wp_value_fupd. by iIntros "$".
   }
   move => K Ks IH Φ.
   have [Ks' HKs']:= W.ectx_item_correct [K].