diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 3b36a4855460a93bdea15778fcc2c74ffdbe13bc..f09b5a9e86391325dd17ac9475ab612865e90571 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2020-12-04.5.b008a6b2") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2020-12-04.7.68955c65") | (= "dev") }
   "coq-autosubst" { = "dev" }
   "coq-iris-string-ident"
 ]
diff --git a/theories/barrier/proof.v b/theories/barrier/proof.v
index f0f40d5e14442881ebe5c1e5dcca42e3d1b6a868..df6a26298ace059fe4a5f7558a61bf7cef4e922b 100644
--- a/theories/barrier/proof.v
+++ b/theories/barrier/proof.v
@@ -50,7 +50,7 @@ Proof. solve_proper. Qed.
 Lemma newbarrier_spec (P : iProp Σ) :
   {{{ True }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
 Proof.
-  iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam. wp_alloc l as "Hl".
+  iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l as "Hl".
   iApply ("HΦ" with "[> -]").
   iMod (saved_prop_alloc P) as (γsp) "#Hsp".
   iMod (own_alloc (● GSet {[ γsp ]} ⋅ ◯ GSet {[ γsp ]})) as (γ) "[H● H◯]".
diff --git a/theories/concurrent_stacks/concurrent_stack1.v b/theories/concurrent_stacks/concurrent_stack1.v
index 724a64337f8b52d721b30ea4518a379f4572f102..44ae7cd3230e1d3104775efc23138cab9110ac7c 100644
--- a/theories/concurrent_stacks/concurrent_stack1.v
+++ b/theories/concurrent_stacks/concurrent_stack1.v
@@ -92,7 +92,6 @@ Section stacks.
     {{{ True }}} new_stack #() {{{ s, RET s; is_stack P s }}}.
   Proof.
     iIntros (ϕ) "_ Hpost".
-    iApply wp_fupd.
     wp_lam.
     wp_alloc ℓ as "Hl".
     iMod (inv_alloc N ⊤ (stack_inv P #ℓ) with "[Hl]") as "Hinv".
diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v
index 4a194fc9ff092c74e62e7b97a920a3d8381bfe09..1b36d8de561c0fba6f532fba8b68f2cc61380caf 100644
--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
@@ -82,7 +82,6 @@ Section side_channel.
     {{{ P v }}} mk_offer v {{{ o γ, RET o; is_offer γ P o ∗ revoke_tok γ }}}.
   Proof.
     iIntros (Φ) "HP HΦ".
-    rewrite -wp_fupd.
     wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc N _ (stages γ P l v) with "[Hl HP]") as "#Hinv".
@@ -162,7 +161,6 @@ Section mailbox.
     {{{ True }}} mk_mailbox #() {{{ v, RET v; is_mailbox P v }}}.
   Proof.
     iIntros (Φ) "_ HΦ".
-    rewrite -wp_fupd.
     wp_lam.
     wp_alloc l as "Hl".
     iMod (inv_alloc N _ (mailbox_inv P l) with "[Hl]") as "#Hinv".
@@ -299,7 +297,6 @@ Section stack_works.
     {{{ True }}} new_stack #() {{{ v, RET v; is_stack P v }}}.
   Proof.
     iIntros (ϕ) "_ Hpost".
-    rewrite -wp_fupd.
     wp_lam.
     wp_alloc l as "Hl".
     wp_apply mk_mailbox_works; first done.
diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v
index 5a3506bbbc4bd4b16edd7e993ffd8004d9bd6fd1..c8959227778ab3895f8d2afeca478903f9354e03 100644
--- a/theories/concurrent_stacks/concurrent_stack3.v
+++ b/theories/concurrent_stacks/concurrent_stack3.v
@@ -97,7 +97,6 @@ Section stack_works.
     {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack_pred P v }}}.
   Proof.
     iIntros (Φ) "HP HΦ".
-    rewrite -wp_fupd.
     wp_lam. wp_alloc l as "Hl".
     iMod (inv_alloc N _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
     { iNext; iExists None, []; iFrame. }
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index efac94f2250e5ab882508c5a7db28631316fbf1e..0d600a2b74d17eaf3d5d73e197bf122527c25211 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -105,7 +105,6 @@ Section proofs.
     {{{ o γ, RET o; is_offer γ P Q o ∗ revoke_tok γ }}}.
   Proof.
     iIntros (Φ) "HP HΦ".
-    rewrite -wp_fupd.
     wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc Nside_channel _ (stages γ P Q l v) with "[Hl HP]") as "#Hinv".
@@ -192,7 +191,7 @@ Section proofs.
     {{{ True }}} mk_mailbox #() {{{ v, RET v; is_mailbox P v }}}.
   Proof.
     iIntros (Φ) "_ HΦ".
-    rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
+    wp_lam. wp_alloc l as "Hl".
     iMod (inv_alloc Nmailbox _ (mailbox_inv P l) with "[Hl]") as "#Hinv".
     { iNext; by iLeft. }
     iModIntro.
@@ -320,7 +319,6 @@ Section proofs.
     {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack_pred P v }}}.
   Proof.
     iIntros (Φ) "HP HΦ".
-    rewrite -wp_fupd.
     wp_lam.
     wp_alloc l as "Hl".
     wp_apply mk_mailbox_works ; first done. iIntros (v) "#Hmailbox".
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index f9e8363e36df204852b29e8e946fa8733033bc00..6401ea0c737bfd0241529b50c9e4a98edffc5e33 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -220,7 +220,7 @@ Section contents.
     {{{ γ γ' t, RET t; isTask r γ γ' t P Q ∗ task γ γ' t a P Q }}}.
   Proof.
     iIntros (Φ) "[#Hrunner HP] HΦ".
-    wp_rec. wp_pures. iApply wp_fupd.
+    wp_rec. wp_pures.
     wp_alloc res as "Hres".
     wp_alloc status as "Hstatus".
     iMod (new_pending) as (γ) "[Htoken Htask]".
@@ -391,7 +391,7 @@ Section contents.
     {{{ γb r, RET r; runner γb P Q r }}}.
   Proof.
     iIntros (Φ) "#Hf HΦ".
-    unfold newRunner. iApply wp_fupd.
+    unfold newRunner.
     wp_lam. wp_pures.
     wp_bind (newBag b #()).
     iApply (newBag_spec b (N.@"bag") (λ x y, ∃ γ γ', isTask (f,x) γ γ' y P Q)%I); auto.
@@ -400,7 +400,6 @@ Section contents.
     iAssert (runner γb P Q (PairV f bag))%I with "[]" as "#Hrunner".
     { rewrite runner_unfold. iExists _,_. iSplit; eauto. }
     iApply (loop_spec n 0 with "Hrunner [HΦ]"); eauto.
-    iNext. iIntros (r) "Hr". by iApply "HΦ".
   Qed.
 
   Lemma runner_Fork_spec γb (r a:val) P Q :
diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v
index 28ec9c34d708bfc6b77a708228e2578ca89661dd..3db9c0cb6295bb6867b7743a30950e25e9be015a 100644
--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -132,7 +132,7 @@ Section proof.
     {{{ x γ, RET x; is_bag γ x ∗ bag_contents γ ∅ }}}.
   Proof.
     iIntros (Φ) "_ HΦ".
-    unfold newBag. wp_rec. iApply wp_fupd.
+    unfold newBag. wp_rec.
     wp_alloc r as "Hr".
     iMod (own_alloc (1%Qp, to_agree ∅)) as (γb) "[Ha Hf]"; first done.
     iMod (inv_alloc N _ (bag_inv γb r) with "[Ha Hr]") as "#Hinv".
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index e221d4a02d2bb670525a30ee5350c19fd9806103..a35bcd31764612636363c9d23d2f932f616e15df 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -264,7 +264,7 @@ Section monotone_counter.
   Lemma newCounter_spec: {{{ True }}} newCounter #() {{{ v, RET #v; isCounter v 0 }}}.
   Proof.
     iIntros (Φ) "_ HCont".
-    rewrite /newCounter -wp_fupd. (* See comment below for why we used wp_fupd. *)
+    rewrite /newCounter.
     wp_lam.
     (* We allocate ghost state using the rule/lemma own_alloc. Since the
        conclusion of the rule is under a modality we wrap the application of
@@ -275,10 +275,7 @@ Section monotone_counter.
     iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γ) "[HAuth HFrac]".
     - apply mcounterRA_valid_auth_frag; auto. (* NOTE: We use the validity property of the RA we have constructed. *)
     - wp_alloc ℓ as "Hpt".
-      (* We now allocate an invariant. For this it is crucial we have used the
-         wp_fupd lemma above to have the Φ under a modality. Otherwise we would
-         have been stuck here, since allocating an invariant is only possible
-         under the fancy update modality. *)
+      (* We now allocate an invariant. *)
       iMod (inv_alloc N _ (counter_inv ℓ γ) with "[Hpt HAuth]") as "HInv".
       + iExists 0%nat; iFrame.
       + iApply ("HCont" with "[HFrac HInv]").
@@ -465,7 +462,7 @@ Section monotone_counter'.
   Lemma newCounter_spec': {{{ True }}} newCounter #() {{{ v, RET #v; isCounter' v (MaxNat 0) }}}.
   Proof.
     iIntros (Φ) "_ HCont".
-    rewrite /newCounter -wp_fupd.
+    rewrite /newCounter.
     wp_lam.
     iMod (own_alloc (● MaxNat 0 ⋅ ◯ MaxNat 0)) as (γ) "[HAuth HFrac]".
     - apply mcounterRA_valid_auth_frag'; auto.
@@ -612,7 +609,7 @@ Section ccounter.
         newCounter #()
     {{{ γ ℓ, RET #ℓ; is_ccounter γ ℓ 1 0%nat }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newCounter /=. wp_lam. wp_alloc ℓ as "Hpt".
+    iIntros (Φ) "_ HΦ". rewrite /newCounter /=. wp_lam. wp_alloc ℓ as "Hpt".
     iMod (own_alloc (●F O%nat ⋅ ◯F 0%nat)) as (γ) "[Hγ Hγ']"; first by apply auth_both_valid_discrete.
     iMod (inv_alloc N _ (ccounter_inv γ ℓ) with "[Hpt Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
diff --git a/theories/lecture_notes/lock.v b/theories/lecture_notes/lock.v
index 23554be3ca06b23faae078b261976b77e736b837..adbd9d8e4663f43cf92e8b9588ae2a19950f3215 100644
--- a/theories/lecture_notes/lock.v
+++ b/theories/lecture_notes/lock.v
@@ -72,7 +72,7 @@ Section lock_spec.
     {{{ P }}} newlock #() {{{ l, RET l; ∃ γ, is_lock γ l P }}}.
   Proof.
     iIntros (φ) "Hi Hcont".
-    rewrite -wp_fupd /newlock.
+    rewrite /newlock.
     wp_lam.
     wp_alloc l as "HPt".
     iMod (own_alloc (Excl ())) as (γ) "Hld"; first done.
diff --git a/theories/lecture_notes/lock_unary_spec.v b/theories/lecture_notes/lock_unary_spec.v
index 2fc8ffe5c2ff70c022397e4e91b553d5dead347b..dc4aea9dcc1de00720709e4367e3fd4d65f6fbcb 100644
--- a/theories/lecture_notes/lock_unary_spec.v
+++ b/theories/lecture_notes/lock_unary_spec.v
@@ -87,7 +87,7 @@ Section lock_spec.
     {{{ True }}} newlock #() {{{v, RET v; ∃ (l: loc) γ, ⌜v = #l⌝ ∧ (∀ P E, P ={E}=∗ is_lock γ l P) }}}.
   Proof.
     iIntros (φ) "Hi Hcont".
-    rewrite -wp_fupd /newlock.
+    rewrite /newlock.
     wp_lam.
     wp_alloc l as "HPt".
     iApply "Hcont".
@@ -147,7 +147,7 @@ Section lock_spec.
     True ⊢ WP newlock #() {{v, ∃ (l: loc) γ, ⌜v = #l⌝ ∧ (∀ P E, P ={E}=∗ is_lock γ l P) }}.
   Proof.
     iIntros "_".
-    rewrite -wp_fupd /newlock.
+    rewrite /newlock.
     wp_lam.
     wp_alloc l as "HPt".
     iExists l.
diff --git a/theories/lecture_notes/modular_incr.v b/theories/lecture_notes/modular_incr.v
index c209851d54532dab576de275382a45b082ed3e2d..b9f972f599832ed8ab652a5c37ec5c710533282a 100644
--- a/theories/lecture_notes/modular_incr.v
+++ b/theories/lecture_notes/modular_incr.v
@@ -126,7 +126,6 @@ Section cnt_spec.
     {{{ True }}} newcounter #m @ E {{{ (ℓ : loc), RET #ℓ; ∃ γ, Cnt ℓ γ ∗ γ ⤇½ m}}}.
   Proof.
     iIntros (Hsubset Φ) "#Ht HΦ".
-    rewrite -wp_fupd.
     wp_lam.
     wp_alloc ℓ as "Hl".
     iApply "HΦ".
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index 0e281a4a8ca2eaa326ea35c0afa0c595b254f319..cb0161ad07585a600aba9e3ae42c0bd0f72247ae 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -172,7 +172,7 @@ Section stack.
   Lemma new_stack_spec :
     {{{ True }}} new_stack #() {{{ γs s, RET s; is_stack γs s ∗ stack_content γs [] }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam.
+    iIntros (Φ) "_ HΦ". wp_lam.
     wp_apply alloc_spec; first done. iIntros (head) "Hhead". wp_let.
     wp_apply alloc_spec; first done. iIntros (offer) "Hoffer". wp_let.
     iMod (own_alloc (● Excl' [] ⋅ ◯ Excl' [])) as (γs) "[Hs● Hs◯]".
diff --git a/theories/logatom/flat_combiner/peritem.v b/theories/logatom/flat_combiner/peritem.v
index a23623a6c3037f8e1d02cab241a7dd445c25bf87..27d133202a4b65c8ceb281b8e35e5c2f6a81b123 100644
--- a/theories/logatom/flat_combiner/peritem.v
+++ b/theories/logatom/flat_combiner/peritem.v
@@ -49,7 +49,7 @@ Section proofs.
   Lemma new_bag_spec:
     {{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". iApply wp_fupd.
+    iIntros (Φ) "_ HΦ".
     wp_lam. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
     wp_alloc s as "Hs".
     iAssert ((∃ xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index 9bd22ad3e22600b346fd12316ea988dbf209eb6c..3f278c7c00c143f42d79fca9ed7646ff01583ab5 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -1482,7 +1482,7 @@ Lemma new_queue_spec sz :
     new_queue #sz
   {{{ v γ, RET v; is_hwq sz γ v ∗ hwq_cont γ [] }}}.
 Proof.
-  iIntros (Hsz Φ) "_ HΦ". wp_lam. wp_apply wp_fupd.
+  iIntros (Hsz Φ) "_ HΦ". wp_lam.
   (** Allocate [q.ar], [q.back] and [q.p]. *)
   wp_apply wp_allocN; [ lia | done | iIntros (ℓa) "[Hℓa _]" ].
   wp_alloc ℓb as "Hℓb".
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 8b856f6944434a0490c97b99cd177ac936baaff8..60ca60a54f7b5d9724e13e79e0c82481fd5e4da0 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -130,7 +130,6 @@ Section atomic_snapshot.
   Proof.
     iIntros (Φ _) "Hx". rewrite /new_snapshot. wp_lam.
     repeat (wp_proj; wp_let).
-    iApply wp_fupd.
     wp_alloc lx' as "Hlx'".
     wp_alloc lx as "Hlx".
     set (Excl' v) as p.
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index 1b3cbf963ecf6bb0b74dfabc6a34a5d8e1c38daf..939bb31c77bae7e600a9395d663228c5baa14664 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -215,8 +215,6 @@ Proof.
   (* Introduce things into the Coq and Iris contexts. Throw away the [True]
      precondition. *)
   iIntros (Φ) "_ HΦ".
-  (* We introduce the fancy update modality in our WP (necessary later). *)
-  iApply wp_fupd.
   (* We step through the program: β-reduce and allocate a location [ℓ]. *)
   wp_lam. wp_alloc ℓ as "Hl". (* We have full ownership of [ℓ] in [Hl]. *)
   (* We now need to establish the invariant. First, we allocate an instance of